../ AbsSyntax.hscleanups13 years ago AbsSyntaxTree.hsAllow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.13 years ago Compiler.hsmake TT aware of Set -> Type14 years ago Completion.hsremove duplicate 'intro' and 'intros'13 years ago Coverage.hsNew size change graph builder Looks at patterns, rather than case tree, and therefore finds it easier to spot structurally smaller arguments which are more complex.13 years ago DSL.hsChange meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.15 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.hsBeginnings of integer SIMD support (no backend yet)13 years ago ElabTerm.hsMerge pull request #383 from JanBessai/ITChar13 years ago Error.hsMake the type of ierror more general13 years ago Help.hsadd command to change current directory14 years ago IBC.hsMerge pull request #383 from JanBessai/ITChar13 years ago IdeSlave.hscleanups13 years ago Imports.hsAdding support for Windows MingW3214 years ago Parser.hsMerge pull request #383 from JanBessai/ITChar13 years ago Primitives.hsCleanup13 years ago Prover.hscleanups13 years ago Providers.hsRemove unused import13 years ago REPL.hsReport success or failure in IDESlave mode while loading a file13 years ago REPLParser.hssquash potential space leaks by using strict foldl14 years ago Transforms.hsuppercase modulenames14 years ago Unlit.hsFix Unlit to cope with documentation comment syntax14 years ago UnusedArgs.hsRemove the unused arg from lookup functions14 years ago