Working through the prelude and fixing bugs/adding functionality to the typechecker to get everything to typecheck. So far this PR:
extends the equality logic to account for the eta-expansion rule for structs (to typecheck e.g. PLift.up_down)
adds isNotZero RHS check to the reduction of Univ.imax a b (to typecheck e.g. DecidableRel)
refactors the typechecker, adding state so that derefConst returns a constant with annotated types/values when one is available (and adds a call to checkConst in the .const case of infer, to typecheck e.g. Subtype.property)
adds support for primitive operations on natural numbers (Nat.add, Nat.mul, Nat.pow, Nat.decEq)
Working through the prelude and fixing bugs/adding functionality to the typechecker to get everything to typecheck. So far this PR:
PLift.up_down)isNotZeroRHS check to the reduction ofUniv.imax a b(to typecheck e.g.DecidableRel)derefConstreturns a constant with annotated types/values when one is available (and adds a call tocheckConstin the.constcase ofinfer, to typecheck e.g.Subtype.property)Nat.add,Nat.mul,Nat.pow,Nat.decEq)