Subtyping, Set Theory and Well Definedness

Tasks

• Rename Document.Expression to Logic.Expr.Parser
• Clean up the Logic.Expr.Parser API
• Generalize Sequent so that, after applying monotonicity in the theorem prover, the goal is a non-empty list of predicates each of which can benefit from removing universals and "stabbing the onion"
• Separate expression parsing from type checking
• Make it easy to change the type system (not necessarily dynamically)
• Draw contract

Goals

• have records as subtypes of functions
• have tuples as subtypes of lists, themselves subtypes of functions
• have natural numbers as subtypes of Int, Rat, Real, Complex, Number