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

6325 commits

Author SHA1 Message Date
Sebastian Ullrich
eceac9f12a perf: avoid syntax stack copy at orelseFn 2023-07-28 08:36:33 -07:00
Scott Morrison
b3fa4fd053 chore: revert #2317 2023-07-28 08:33:49 -07:00
Wojciech Nawrocki
74e0f09009
fix: handle error in withTraceNode message action (#2364) 
* fix: handle error in withTrace message action

* Update src/Lean/Util/Trace.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* Update Trace.lean

---------

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
 2023-07-28 08:01:13 -07:00
Sebastian Ullrich
aeb60764c1 feat: auto-complete declaration names in arbitrary namespaces 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
687f50ab33 fix: never show private names in completion 2023-07-28 07:50:09 -07:00
Sebastian Ullrich
b15d6d41b8 fix: missing mkCIdents in Lean.Elab.Deriving.Util 2023-07-28 07:48:34 -07:00
Siddharth Bhat
073c8fed86 feat: LLVM backend: support for visibility Style & DLL storage 
Changes peeled from:
https://github.com/leanprover/lean4/pull/2340

to allow a `stage0` bump on master before merging in the
changes that allow LLVM to build in stage1+.
 2023-07-25 11:03:16 +02:00
Alex J Best
808bb9b579
perf: dont repeatedly elab term in rw at multiple locations #2317 2023-07-24 08:47:52 -07:00
Jannis Limperg
6407197e54 chore: better error message for loose bvar in whnf 2023-07-20 13:47:20 -07:00
Wojciech Nawrocki
e1b3f10250 doc: fix contradictory docstring 2023-07-19 10:53:47 +02:00
Leonardo de Moura
634193328b fix: fixes #2327 2023-07-18 07:18:27 -07:00
Leonardo de Moura
212cd9c3e6 fix: fixes #2321 2023-07-13 14:41:32 -07:00
Scott Morrison
0d5c5e0191 feat: relax test in checkLocalInstanceParameters to allow instance implicits 2023-07-13 10:54:06 -07:00
Leonardo de Moura
6d857a93b5 perf: pointer set for traversing DAGs 2023-07-11 19:19:42 -07:00
Mario Carneiro
76023a7c6f fix: don't run [builtin_init] when builtin = false 2023-07-10 08:58:02 -07:00
Sebastian Ullrich
c268d7e97b fix: kill descendant processes on worker exit 2023-07-05 23:42:53 +02:00
Mario Carneiro
f1b2a8acce fix: lazy_binop + coercion bug 
fixes #2300
 2023-07-01 06:05:25 -07:00
Leonardo de Moura
94d4a427e2 fix: fixes #2115 2023-06-30 19:54:38 -07:00
Leonardo de Moura
a002ce6d0d fix: fixes #2077 2023-06-30 19:26:00 -07:00
Leonardo de Moura
ec42581d1f perf: use Core.transform instead of Meta.transform at betaReduceLetRecApps 
Observed big performance improvement on files containing big proofs
generated using tactics.
 2023-06-28 12:29:12 -07:00
Leonardo de Moura
eece499da9 fix: fixes #2282 2023-06-27 16:46:38 -07:00
Sebastian Ullrich
f0583c3fd6 feat: trace nodes for SizeOf and injectivity theorem generation 2023-06-27 16:17:46 -07:00
Wojciech Nawrocki
ba4bfe26f2 fix: add missing instantiateMVars 2023-06-27 16:13:56 -07:00
Sebastian Ullrich
e1999ada7f fix: make "elaboration" metric work in language server 2023-06-27 15:56:34 +01:00
Leonardo de Moura
4036be4f50 fix: add missing check at IR checker 2023-06-23 08:43:39 -07:00
Mario Carneiro
123c1ff7f0 fix: basic ident fallback in identComponents 2023-06-22 09:50:24 +01:00
Mario Carneiro
e0893b70e5 fix: incorrect type for SpecInfo.argKinds 2023-06-21 22:50:29 -07:00
Leonardo de Moura
425f42cd83 feat: better support for Nat literals at DiscrTree.lean 2023-06-21 22:30:09 -07:00
Leonardo de Moura
bebf1927f8 chore: remove workarounds 2023-06-21 20:35:33 -07:00
Leonardo de Moura
184f2ed597 chore: improve isNonTrivialProof 2023-06-21 20:28:17 -07:00
Leonardo de Moura
7367f2edc6 fix: unfold constant theorems when transparency is set to .all 2023-06-21 20:28:17 -07:00
Leonardo de Moura
9df2f6b0c9 fix: bump transparency to .all when reducing the major premise of Acc.rec and WellFounded.rec 2023-06-21 20:28:17 -07:00
Leonardo de Moura
2b8e55c2f1 fix: Nat literal bug at DiscrTree.lean 2023-06-21 20:28:17 -07:00
Leonardo de Moura
d6695a7a2e fix: use mkAuxTheoremFor when creating helper proof_n theorems 2023-06-21 20:28:17 -07:00
Scott Morrison
a44dd71ad6 feat: add flag for apply to defer failed typeclass syntheses as goals 2023-06-19 20:07:07 -07:00
Scott Morrison
82196b5b94
feat: allow upper case single character identifiers when relaxedAutoImplicit false (#2277) 
* feat: allow upper case single character identifiers when relaxedAutoImplicit false

* update tests

* fix tests

* fix another test

---------

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
 2023-06-19 20:04:09 -07:00
Mario Carneiro
2348fb37d3 fix: use Lean.initializing instead of IO.initializing 2023-06-17 06:57:14 -07:00
Mario Carneiro
e64a2e1a12 fix: misleading indentation 2023-06-17 06:56:53 -07:00
Gabriel Ebner
bff612e59e fix: simp: synthesize non-inst-implicit tc args 
Fixes #2265.
 2023-06-09 16:32:02 -07:00
Mario Carneiro
1ac8a4083f feat: report section name in invalid end msg 2023-06-09 14:41:39 -07:00
Mario Carneiro
b4cf1dd943 feat: binder info for generalize 2023-06-09 14:41:00 -07:00
Mario Carneiro
b139a97825 fix: hygieneInfo should not consume whitespace 2023-06-09 15:05:19 +02:00
Sebastian Ullrich
451ccec154 fix: save when used as last tactic 2023-06-07 14:29:45 -07:00
Sebastian Ullrich
7987b795bb fix: workspace symbols 
Somehow was broken by #2233
 2023-06-06 14:58:24 +02:00
Sebastian Ullrich
90e2288187 fix: interpret initializers in order 2023-06-05 15:46:35 -07:00
Sebastian Ullrich
97cffd4711 fix: prefer resolving parser alias over declaration 2023-06-05 16:52:23 +02:00
Mario Carneiro
a8d6178e19 feat: implement have this (part 2) 2023-06-02 16:19:02 +02:00
Mario Carneiro
43f6d0a761 feat: implement have this (part 1) 2023-06-02 16:19:02 +02:00
Mario Carneiro
c20a7bf305 feat: hygieneInfo parser (aka this 2.0) 2023-06-02 16:19:02 +02:00
Henrik
28538fc748 feat: trace nodes for kernel type checking 2023-05-31 06:10:26 -07:00