max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
29758 commits 1 branch 0 tags 5.3 GiB
Commit graph

4 commits

Author SHA1 Message Date
Leonardo de Moura
e6f5b3758c feat: precompute folders 2022-09-26 21:10:38 -07:00
Leonardo de Moura
1e75001405 feat: preserve user provided names at LCNF Simp 
It helps preserving let-declaration names in pure code, but it is not
very useful for monadic let-decls (e.g., `let x <- act`). The binder
names are often lost we eliminating the abstraction layers.
 2022-09-26 21:04:13 -07:00
Henrik Böving
2958b8a7f5 feat: basic constant folder 
supports:
- arithmetic operations:
  - folding full constants
  - folding neutral elements
  - folding annihilators
- List.toArray
 2022-09-26 21:03:47 -07:00
Leonardo de Moura
35ca2b203c refactor: split Simp.lean 2022-09-26 07:04:20 -07:00