lean4-htt/tests
Leonardo de Moura e9d85f49e6 chore: remove tryPureCoe?
Based on the discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574
The consensus seemed to be that "auto pure" is more confusing than its worth.
2022-02-03 16:25:24 -08:00
..
bench chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
compiler chore: fix tests 2022-01-15 12:18:09 -08:00
elabissues
ir
lean chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
leanpkg chore: remove tryPureCoe? 2022-02-03 16:25:24 -08:00
playground feat: add procedure for solving subgoals generated by mkSplitterProof 2021-08-24 20:23:13 -07:00
plugin
simpperf
.gitignore
common.sh chore: replace sed with perl in test driver 2021-09-16 21:33:56 +02:00