michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/init/tactic): typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-24 16:10:35 -08:00
parent 1924b2884c
commit c85d6d5a1e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/tactic.lean
View file

@ -21,7 +21,7 @@ namespace tactic
-- a term of type 'tactic' into a tactic that sythesizes a term -- a term of type 'tactic' into a tactic that sythesizes a term
definition and_then (t1 t2 : tactic) : tactic := builtin definition and_then (t1 t2 : tactic) : tactic := builtin
definition or_else (t1 t2 : tactic) : tactic := builtin definition or_else (t1 t2 : tactic) : tactic := builtin
definition append (t1 t2 : tactic) : tactic := builtin definition par (t1 t2 : tactic) : tactic := builtin
definition fixpoint (f : tactic → tactic) : tactic := builtin definition fixpoint (f : tactic → tactic) : tactic := builtin
definition repeat (t : tactic) : tactic := builtin definition repeat (t : tactic) : tactic := builtin
definition at_most (t : tactic) (k : num) : tactic := builtin definition at_most (t : tactic) (k : num) : tactic := builtin