../ AbsSyntax.hsAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.13 years ago AbsSyntaxTree.hsrename O into Z13 years ago Compiler.hsmake TT aware of Set -> Type14 years ago Completion.hsAdd primitive vector types to REPL autocompletion13 years ago Coverage.hsMuch faster coverage checking by ignorng forced arguments No need to generate cases to check for them, because we already know their value is forced by another part of the same constructor!13 years ago DSL.hsAllow names to be attached to provisional definitions lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent.13 years ago DataOpts.hsRemove the unused arg from lookup functions14 years ago Delaborate.hsImprove the "...is not solved" internal error to display something useful Fixes #361 Fixes #32113 years ago Docs.hsRemove the unused arg from lookup functions14 years ago ElabDecls.hsAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.13 years ago ElabTerm.hsFix let scope leakage bug13 years ago Error.hsMake the type of ierror more general13 years ago Help.hsadd command to change current directory14 years ago IBC.hsAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.13 years ago IdeSlave.hscleanups13 years ago Imports.hsAdding support for Windows MingW3214 years ago Parser.hsAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.13 years ago PartialEval.hsAdd %specialise annotation for functions (Part 1 of partial evaluation) %specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. T…13 years ago Primitives.hsFix interpreter implementation of signed operations on Integer13 years ago Prover.hscleanups13 years ago Providers.hsRemove unused import13 years ago REPL.hsSpecial case for displaying Type : Type 1 ...because people get the wrong impression about universes otherwise!13 years ago REPLParser.hssquash potential space leaks by using strict foldl14 years ago Transforms.hsrename O into Z13 years ago Unlit.hsFix Unlit to cope with documentation comment syntax14 years ago UnusedArgs.hsRemove the unused arg from lookup functions14 years ago