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

8539 commits

Author SHA1 Message Date
Floris van Doorn
1a6663a41b
chore: write "|-" as "|" noWs "-" (#2299) 
* remove |- as an alias for ⊢

* revert false positive |->

* fix docstring

* undo previous changes

* [unchecked] use suggestion

* next attempt

* add test
 2023-07-14 09:48:20 -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
fd0549feb5 chore: improve test 2023-07-11 19:19:42 -07:00
Leonardo de Moura
6d857a93b5 perf: pointer set for traversing DAGs 2023-07-11 19:19:42 -07:00
Leonardo de Moura
5402c3cf76 chore: fix test file names 2023-07-01 06:20:36 -07: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
Leonardo de Moura
2b8e55c2f1 fix: Nat literal bug at DiscrTree.lean 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
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
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
c20a7bf305 feat: hygieneInfo parser (aka this 2.0) 2023-06-02 16:19:02 +02:00
Mario Carneiro
e826f5f42a fix: spacing around calc 2023-06-02 09:15:15 +02:00
Mario Carneiro
5661b15e35 fix: spacing and indentation fixes 2023-05-28 18:48:36 -07:00
Leonardo de Moura
83cc0bcc96 fix: fixes #2199 2023-05-28 18:29:09 -07:00
Jannis Limperg
c84690028b fix: ignore implDetail hyps in withLocation 2023-05-28 17:40:55 -07:00
Mario Carneiro
5d3ac5f80c fix: panic in Match.SimpH.substRHS 2023-05-28 17:04:28 -07:00
Gabriel Ebner
ebc32af2e6 chore: fix flaky test 2023-05-15 13:23:38 -07:00
Parth Shastri
555f5f390c fix: stop iterating over visited mvars in collectUnassignedMVars 2023-05-15 09:37:19 -07:00
Parth Shastri
954190e457 fix: remove repeat calls to inferType in ignoreField 2023-05-15 09:35:44 -07:00
Gabriel Ebner
5781752985 fix: offset unification with a+a+1 
Fixes #2136
 2023-05-15 09:06:37 -07:00
Gabriel Ebner
ae2b2c3903 chore: add regression test for mathlib eta perf issue 2023-05-15 09:05:41 -07:00
Gabriel Ebner
1f21ababfa chore: remove etaExperiment option 2023-05-15 09:05:41 -07:00
Gabriel Ebner
41729263c5 fix: tests 2023-05-15 09:05:41 -07:00
Mario Carneiro
ad4b822734 fix: use snake case for @[code_action_provider] 2023-05-08 22:25:48 +02:00
Henrik Böving
0e042d8ef6 fix: LCNF simp forgot to mark normalized decls as simplified 2023-05-05 12:17:26 -07:00
Henrik Böving
a6ae661195 feat: profiling of linters 2023-04-18 15:30:21 +02:00
Sebastian Ullrich
8a302e6135 fix: match discriminant reduction should not unfold irreducible defs 2023-04-10 21:09:04 -07:00
Gabriel Ebner
7f51628986 fix: simp: strip mdata when testing for True/False 
Fixes #2173
 2023-04-10 21:06:42 -07:00
Scott Morrison
06c752448b chore: add missing simp lemma (¬ False) = True 2023-04-10 21:05:54 -07:00
Gabriel Ebner
8075d1f45d fix: reset local context in mkInjectiveTheorems 2023-04-10 21:05:16 -07:00
Gabriel Ebner
5eb9688846 chore: flaky tests 2023-04-10 13:00:04 -07:00
Gabriel Ebner
4544443d98 feat: reorder tc subgoals according to out-params 2023-04-10 13:00:04 -07:00
Sebastian Ullrich
427540db45 chore: remove redundant Elab.input trace class in favor of Elab.command 2023-04-10 16:57:54 +02:00
Sebastian Ullrich
bafa4e0a78 feat: use with_trace for important trace classes 2023-04-10 16:57:54 +02:00
Connor Baker
667d54640d
chore: Nix: use strings instead of URL literals (#2172) 2023-03-28 10:10:24 +02:00
int-y1
9bc6fa1c6e chore: fix typos 2023-03-27 10:05:50 +02:00
Sebastian Ullrich
b81cff87bc chore: update temci 2023-03-24 11:34:21 +01:00
Sebastian Ullrich
83c1a1ab77 chore: bench: update temci 2023-03-16 16:39:50 +01:00
Sebastian Ullrich
a62d412dce fix: implement · tacs as a builtin elaborator, part 2 
Fixes #2153
 2023-03-15 17:00:15 +01:00
Sebastian Ullrich
b8cc5b277e fix: strict indentation check in · tacs 2023-03-15 11:33:19 +01:00