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

20431 commits

Author SHA1 Message Date
Sebastian Ullrich
a03749cbe4 fix: findReferences should find only original syntax 2022-09-27 22:09:54 +02:00
Mario Carneiro
d843e2a418 chore: add docs and test 2022-09-27 22:09:54 +02:00
Mario Carneiro
2270e8cd53 fix: ignore unused anonymous have variables 2022-09-27 22:09:54 +02:00
Mario Carneiro
6bf01ebd30 feat: use have token span for implicit this 2022-09-27 22:09:54 +02:00
Mario Carneiro
969eefe79b fix: let _ := should not introduce a variable called "_" 2022-09-27 22:09:54 +02:00
Mario Carneiro
280d8c9c9b feat: add (canonical := true) option in Syntax 2022-09-27 22:09:54 +02:00
Ed Ayers
64e7f25ffe doc: apply suggestions from code review 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-09-27 11:37:49 -07:00
E.W.Ayers
8e085fb637 doc: some documentation for Message.lean 2022-09-27 11:37:49 -07:00
Patrick Massot
f0c8e6fa2d doc: add docstrings in PersistentExtension 
Add docstring to functions with non-obvious persistence properties. See the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/HashMap.20extension/near/300784691
 2022-09-27 10:34:09 -07:00
Leonardo de Moura
f067382f52 chore: remove old exports 2022-09-27 07:44:38 -07:00
Leonardo de Moura
8596e4af88 fix: mark code as simplified 2022-09-26 21:27:45 -07:00
Leonardo de Moura
193e3fd184 feat: add basic String folding 2022-09-26 21:23:08 -07:00
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
Leonardo de Moura
24e584cf00 feat: add Renaming.lean 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
73d5e12ac5 fix: baseExt must not use SimplePersistentEnvExtension 
We invoke `Decl.saveBase` more than once when we update a declaration.
 2022-09-26 08:15:47 -07:00
Leonardo de Moura
ba619be393 fix: apply macroInline again after inlineMatchers 2022-09-26 07:31:27 -07:00
Leonardo de Moura
837ce4374c feat: use reduceJpArity after successful simpJpCases? 2022-09-26 07:25:29 -07:00
Leonardo de Moura
35ca2b203c refactor: split Simp.lean 2022-09-26 07:04:20 -07:00
Mario Carneiro
85119ba9d1 chore: move Std.* data structures to Lean.* 2022-09-26 05:46:04 -07:00
Leonardo de Moura
fd1ae3118c feat: replace isCasesOnCases? with simpJpCases? 
It addresses the code explosion issue with the old optimization.
For example, the resulting size for `Lean.Json.Parser.escapedChar`
went from 31593 to 361.
 2022-09-25 20:57:24 -07:00
Leonardo de Moura
bbac49e925 feat: add collectJpCasesInfo 
Collect statistics for implementing new optimization that will replace `isCasesOnCases?`
 2022-09-25 20:57:24 -07:00
Mario Carneiro
9b9998f5c8 feat: pattern (occs := ...) conv 2022-09-25 19:52:56 -07:00
Leonardo de Moura
dadfe84c15 doc: update const2ModIdx docstring 2022-09-25 14:06:07 -07:00
Leonardo de Moura
236885e72e chore: remove Stage1 2022-09-25 13:17:50 -07:00
Mario Carneiro
5644bd7a3f feat: show decl module in hover 2022-09-25 06:43:48 -07:00
Mario Carneiro
fa13d7321f feat: generalize e = x at h 2022-09-25 06:42:20 -07:00
Mario Carneiro
84497c1d09 feat: sort simp lemmas by application order 2022-09-25 06:40:56 -07:00
Mario Carneiro
afca560bda chore: revert builtin flag on Origin 2022-09-25 06:40:56 -07:00
Mario Carneiro
b739186e98 feat: use a structured type for simp theorem Origin 2022-09-25 06:40:56 -07:00
Mario Carneiro
97bcc7fd7c feat: add ForM -> ForIn adapter 2022-09-25 06:40:56 -07:00
Mario Carneiro
9550db0e3b chore: remove fvarIdToLemmaId 2022-09-25 06:40:56 -07:00
Mario Carneiro
606328aceb feat: improve simp theorem tracing 2022-09-25 06:40:56 -07:00
Mario Carneiro
9a9f3263d4 feat: add tactic.simp.trace option 2022-09-25 06:40:56 -07:00
Mario Carneiro
7dc0e1aa7d fix: tweak formatter spacing for tactics 2022-09-25 06:40:56 -07:00
Mario Carneiro
0961561d4e feat: track simp lemmas through the core tactics 2022-09-25 06:40:56 -07:00
Mario Carneiro
687f1c2271 refactor: make simp lemma names mandatory 2022-09-25 06:40:56 -07:00
Leonardo de Moura
afb457ca2a feat: add forEachDecl for LCNF 2022-09-24 20:18:27 -07:00
Leonardo de Moura
ce12ecfe13 fix: free variable collision at LCNF/Specialize.lean 2022-09-24 18:51:32 -07:00
Leonardo de Moura
5969dc2694 feat: beta-reduce at LCNF normExpr 2022-09-24 18:26:34 -07:00
Leonardo de Moura
f7a1429cfd feat: improve ppDecl' 2022-09-24 18:09:43 -07:00
Leonardo de Moura
c858aa3088 feat: replace getStage1Decl? with new getDecl? 2022-09-24 15:00:19 -07:00
Leonardo de Moura
ce90e98648 feat: activate new compiler first phase 2022-09-24 14:20:21 -07:00
Leonardo de Moura
33fdde9b22 fix: LCNF compatibleTypes 
Missing rules:
`⊤ a` is compatible with anything.
`◾ a` is compatible with anything.
 2022-09-24 14:20:21 -07:00
Leonardo de Moura
7ca7139fe8 fix: incorrect [inline] annotation 2022-09-24 14:20:21 -07:00
Leonardo de Moura
e51b078015 fix: incorrect annotations 2022-09-24 14:20:21 -07:00
Leonardo de Moura
6343b97acb feat: display inlining stack when maximum recursion depth has been reached 2022-09-24 14:20:21 -07:00
Leonardo de Moura
7d583f9543 fix: convert _unsafe_rec to original name 2022-09-24 08:19:41 -07:00
Leonardo de Moura
b88bd98afa fix: unreach case for Code.bind 2022-09-24 08:13:17 -07:00