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

7512 commits

Author SHA1 Message Date
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
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
int-y1
9bc6fa1c6e chore: fix typos 2023-03-27 10:05:50 +02: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
Sebastian Ullrich
4cc6057f4a chore: ensure consistent (Unix) encoding for source files 2023-03-10 16:27:56 +01:00
Sebastian Ullrich
51e77d152c fix: do not inherit file handles across process creation 2023-03-10 16:27:56 +01:00
Sebastian Ullrich
d4caf1f922 fix: $_* anonymous suffix splice syntax pattern 2023-03-06 16:30:18 +01:00
Gabriel Ebner
0da281fab4 fix: reject occurrences of inductive type in index 
Fixes #2125
 2023-02-28 12:22:54 -08:00
Adrien Champion
473486eeb9 fix: calc indentation and allow underscore in first relation 2023-02-23 14:20:21 -08:00
Sebastian Ullrich
3f6c5f17db fix: unhygiene in expandExplicitBinders 2023-02-22 17:07:31 +01:00
Gabriel Ebner
7992ce6b4d chore: add test for calc 2023-02-21 16:41:46 -08:00
Gabriel Ebner
adcca17991 chore: add option to enable structure eta in tc search 2023-02-21 16:41:30 -08:00
Gabriel Ebner
75252d2b85 perf: whnf projections during defeq 2023-02-09 19:54:23 -08:00
Gabriel Ebner
448f49ee91 Revert "fix: reenable structure eta during tc search" 
The fix is blocked by slow defeq checks for TC instances; see issues
1986 and 2055.  Enabling it right now causes lots of timeouts in
mathlib4.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bump.20to.202023-02-06/near/326223768

This reverts commit 15a045ee66.
 2023-02-09 11:37:30 -08:00
Gabriel Ebner
3c562c1a9b fix: unify goal before executing nested tactics in calc 
Fixes #2095
 2023-02-09 11:34:07 -08:00
Gabriel Ebner
15a045ee66 fix: reenable structure eta during tc search 
Fixes #2074.
 2023-02-05 11:41:00 -08:00
Gabriel Ebner
d4b9a532d2 fix: calc: synthesize default instances 
This is necessary to figure out the types with exponentiations.

Fixes #2079
 2023-02-02 14:29:21 -08:00
Gabriel Ebner
8265d8bb13 chore: calc: improve error range 2023-02-02 14:21:06 -08:00
Gabriel Ebner
18b3bd7875 fix: calc: do not take lhs/rhs from expected type 
Fixes #2073
 2023-01-30 15:02:40 -08:00
Gabriel Ebner
e37f209c1a fix: unify types in calc 2023-01-27 13:38:42 -08:00
Leonardo de Moura
decb08858f fix: kernel must ensure that safe functions cannot use partial ones. 
Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meaning.20of.20.60DefinitionSafety.2Epartial.60
 2023-01-27 12:17:37 -08:00
Sebastian Ullrich
d01a521be2 test: fix 2023-01-26 13:31:16 +01:00
Sebastian Ullrich
badfcdc49f fix: missing info tree on elab failure 2023-01-26 13:05:57 +01:00
Sebastian Ullrich
f24608c4d1 fix: make eoi an actual command with info tree 2023-01-26 13:05:57 +01:00
Sebastian Ullrich
8a4059dc65 fix: avoid notation in quotation elaborator output 2023-01-26 13:05:33 +01:00
Sebastian Ullrich
18297d8d91 fix: notation unexpander on overapplication of non-nullary notation 2023-01-26 13:05:33 +01:00
Rishikesh Vaishnav
561e404fe4
feat: make go-to-definition on a typeclass projection application go to the instance(s) (#1767) 2023-01-19 09:10:01 +00:00
Rishikesh Vaishnav
600758ba49
fix: fuzzy-find bonus for matching last characters of pattern and symbol (#1917) 2023-01-19 09:06:53 +01:00
Sebastian Ullrich
43c5ab802f fix: show tactic info on canonical by 2023-01-18 10:23:37 +01:00
Sebastian Ullrich
223f1073d1 chore: info tree format should not leak hygiene IDs 2023-01-16 08:33:58 -08:00
Sebastian Ullrich
d59f5c2ffa fix: binop% info tree 2023-01-16 08:33:58 -08:00
James Gallicchio
65db25bf49
feat: funext no arg tactic (#2027) 
* feat: `funext` no arg tactic

Description of funext tactic includes behavior that is not implemented. This implements the behavior.

* fix

* feat: test new funext tactic

* use repeat for clarity of intent
 2023-01-15 08:53:49 -08:00
Eric Wieser
8cd9ce0684 refactor: redefine Nat.mod such that rfl : 0 % n = 0 
This property was true in Lean 3, and it was very convenient for working with `Fin n`.
 2023-01-11 09:49:58 -08:00
James Gallicchio
37650f9147
fix: add done alternative to decreasing_with (#2019) 
Previously `decreasing_with` failed if `simp_wf` closes the goal on its
own. This can cause undesired regressions when new `simp` lemmas are
introduced.

Closes #2018.
 2023-01-09 09:46:37 -08:00