max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/old_tests/tests
History
Leonardo de Moura 008b7b2ac2 fix(library/noncomputable): bug at is_noncomputable 
In Lean4, the check should be based on the compiler.
That is, a definition should be marked as noncomputable when we cannot
generate code for it.
2018-04-16 14:26:37 -07:00
..
lean fix(library/noncomputable): bug at is_noncomputable 2018-04-16 14:26:37 -07:00
.gitignore