git.iko.soy/Idris-dev
on master help sign in
Merge pull request #774 from david-christiansen/induction-completion

Add tab completion for "induction" in prover

commitb67f1802e11bffa70128516754f3ae864c3b9dc1 authorEdwin Brady <edwin.brady@gmail.com> dateThu 9 Jan 2014, 04:32 (13 years ago) parented969b3f793c7b
1 file changed+1
compare with master
unifiedsplit
src/Idris/Completion.hs+1
src/Idris/Completion.hs+1
@@ -44,6 +44,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
4444 , ("reflect", Just ExprTArg)
4545 , ("fill", Just ExprTArg)
4646 , ("try", Just AltsTArg)
47+ , ("induction", Just NameTArg)
4748 ] ++ map (\x -> (x, Nothing)) [
4849 "intros", "compute", "trivial", "solve", "attack",
4950 "state", "term", "undo", "qed", "abandon", ":q"