Leonardo de Moura 8c6a510e65 fix: use withReducible ... `def17.lean` contains example where `isDefEq arg x` takes a very long time with the default reducibility test.		2021-01-19 18:01:52 -08:00
..
Basic.lean	fix: fixes #282	2021-01-19 18:01:52 -08:00
Main.lean	feat: improve error message position for termination check failures	2021-01-13 10:59:28 -08:00
MkInhabitant.lean	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00
Structural.lean	fix: use withReducible	2021-01-19 18:01:52 -08:00
WF.lean	chore: remove #lang lean4 header	2020-10-25 09:54:07 -07:00