Constraints for "with" and "tcons"

[Alan H]

When making a constraint for a "with" statement, do we return a t-fun
that maps the input type to the output type, or do we just manually
constrain both the parameter and body. The book was...vague on the
subject of constraining "with" statements.

Also, we're told that lists can be a list of numbers or a list of
booleans. Can it also be a list of both? If not, then how do we
generate constraints for tempty?

[Chris Burnham]

We generated constraints for tempty by defining it to be a list of
'something'. Unification will make it match whatever tcons it is a
part of.

We're kind of guessing on 'with'. We said that the type of with would
be constrained to be the type of its body. We constrained the
identifier to be the type of whatever its value is.

[Jesse J]

No, a list can't be both numbers and booleans, because it would then be impossible to determine the type when using tfirst. Also, what Chris said appears to be correct.