max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/tools/mini_crush
History
Sebastian Ullrich d0c2c73b35 refactor(init/meta,tools): rename now tactic to done 
It was pointed out that Coq already uses `now` for a different kind of tactic.
And `done` is more descriptive anyway.
2017-05-03 11:18:31 +02:00
..
default.lean refactor(init/meta,tools): rename now tactic to done 2017-05-03 11:18:31 +02:00
nano_crush.lean refactor(init/meta,tools): rename now tactic to done 2017-05-03 11:18:31 +02:00