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

chore(library/tools/mini_crush/default): increase timeout

Browse source
This commit is contained in:
Leonardo de Moura 2017-04-30 16:27:55 -07:00
parent fc9a8ed3be
commit 701b51a882
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/tools/mini_crush/default.lean
View file

@ -113,7 +113,7 @@ when_tracing `mini_crush $
/- Simple tactic -/
meta def close_aux (hs : hinst_lemmas) : tactic unit :=
triv <|> reflexivity reducible <|> contradiction
<|> try_for 100 (rsimp {} hs >> now) <|> try_for 100 reflexivity
<|> try_for 1000 (rsimp {} hs >> now) <|> try_for 1000 reflexivity
meta def close (hs : hinst_lemmas) (s : name) (e : option expr) : tactic unit :=
now