max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/meta/interactive): improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-27 14:55:10 -07:00
parent d0ab6065c3
commit 09bf8921fe
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/meta/interactive.lean
View file

@ -163,7 +163,7 @@ do e ← to_expr p,
tactic.generalize e x
meta def trivial : tactic unit :=
tactic.triv <|> tactic.reflexivity <|> tactic.contradiction
tactic.triv <|> tactic.reflexivity <|> tactic.contradiction <|> fail "trivial tactic failed"
meta def contradiction : tactic unit :=
tactic.contradiction