Skip to content

Relax SetAdd typing rule analogously to ElementOfSet

Viktor Kuncak requested to merge fix-set-add-typing into master

Created by: gsps

Our typing rule for SetAdd is currently more restrictive than necessary. Namely, we reject judgments of the form

xs : Set[T], x : S  |-  xs + x : Set[T]
where S <: T

while x \in xs passes in the same typing environment. This PR relaxes the typing rule of SetAdd to match the behavior on ElementOfSet.

Merge request reports