../ AbsSyntax.hsFix shadowing bug with dependent pair bindings13 years ago AbsSyntaxTree.hsDelete unused code13 years ago Chaser.hsFix name shadowing in where13 years ago Completion.hsAdd primitive vector types to REPL autocompletion13 years ago Coverage.hsChange TCGen flag to Dictionary, update evaluator accordingly13 years ago DSL.hsAdded 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of au…13 years ago DataOpts.hsRemove the unused arg from lookup functions14 years ago Delaborate.hsResolve names/expand implicits inside refl Fixes #44713 years ago Docs.hsRemove the unused arg from lookup functions14 years ago ElabDecls.hsSimplify evaluator It tries to support too much, but since it's part of the kernel it should do as little clever stuff as possible. Now just normalises, simplifies or specialises, the latter two simply meaning that certain names are blocked from being redu…13 years ago ElabTerm.hsNew module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging ar…13 years ago Error.hsMake the type of ierror more general13 years ago Help.hsadd command to change current directory14 years ago IBC.hsNew module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging ar…13 years ago IdeSlave.hscleanups13 years ago Imports.hsNew module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging ar…13 years ago Parser.hsNew module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging ar…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.hsAdd '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.13 years ago Prover.hsChange TCGen flag to Dictionary, update evaluator accordingly13 years ago Providers.hsRemove unused import13 years ago REPL.hsFix name shadowing in where13 years ago REPLParser.hsIgnore initial whitespace and comments in REPL13 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