max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library
History
Leonardo de Moura 692701c5ef feat(library/init/meta): use cheap "reflexivity" after simp and rewrite 
The idea is to make sure lean doesn't timeout (at reflexivity) when we apply simp or
rewrite in goals such as

    (x y : nat) |- x + y + 10000000000 = x + y + 200000000000000

This commit also addresses an issue raised at #1218
2016-12-08 14:41:26 -08:00
..
algebra chore(*): don't use upper case letter for type variables, and camelCase for declarations 2016-11-17 14:54:08 -08:00
data refactor(library/init): create init.data folder 2016-12-02 14:23:06 -08:00
debugger refactor(library/init/string): do not mark string as reducible 2016-11-23 11:28:20 -08:00
init feat(library/init/meta): use cheap "reflexivity" after simp and rewrite 2016-12-08 14:41:26 -08:00
system feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
.gitignore
.project feat(*): C++ code generator 2016-12-05 16:11:41 -08:00
library.md fix(library/library.md): stray keystroke 2016-11-19 10:25:33 -08:00
standard.lean chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00