on 6469b16 help sign in
all commits
583cc43Add ability to set ANSI italicsDavid Christiansen 1085d22Tab completion for setting colours at the REPLDavid Christiansen c404489Add primitive vector types to REPL autocompletionBenjamin Saunders f540cf5remove duplicate 'intro' and 'intros'Hannes Mehnert c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady 25ae311Add primitive type names to name completionDavid Christiansen c1a4eacFull TT reflection and reificationJan Bessai a029bd8reduce duplication by providing a show instance for CmdArgHannes Mehnert 2297270unify help and completion of REPL - previously they were not in sync, now it is one lookup tableHannes Mehnert 1617dd3Stop completion of names that are prefixes of othersDavid Christiansen 25a4649Only use metavariables as completions for :p and :proveDavid Christiansen 0bcdd51Complete identifiers following non-whitespaceDavid Christiansen 1e86384Haddock for completion moduleDavid Christiansen 66d8360Crude support for completion in proverDavid Christiansen 52203a3Complete tactic names in proverDavid Christiansen cc80288Rename the REPL's Haskeline uses to make them obviously REPL-specificDavid Christiansen cc3c913Complete arguments of commands (though slightly crudely)David Christiansen f0e096bComplete multiple identifiers in one expressionDavid Christiansen fc58a50Simple completion supportDavid Christiansen