../ CaseTree.hsAdd collapsing optimisation and more aggressive erasure14 years ago Constraints.hsFix cyclic universe checking bug14 years ago CoreParser.hsAdded "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.14 years ago Elaborate.hsErase unused arguments when compiling14 years ago Evaluate.hsSeparate "productive" and "total" in totality checker Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet!14 years ago ProofShell.hsA small cleanup after missing some stray ends in the diff.15 years ago ProofState.hsErase unused arguments when compiling14 years ago ShellParser.hsFiddle with elaborator; update interp sample and test15 years ago TT.hsImprove some error messages14 years ago Typecheck.hsImprove some error messages14 years ago Unify.hsWarn when generating a setter for a record fails ...rather than failing (since it may just not work for dependent records)14 years ago