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

18700 commits

Author SHA1 Message Date
Leonardo de Moura
bfe57a1cb0 chore: simplify definition 2022-03-12 20:16:45 -08:00
Leonardo de Moura
5707cab7bf feat: improve #eval command 
Now, if it fails to synthesize the TC instance, it applies `whnf` and
tries again.
 2022-03-12 19:55:15 -08:00
Leonardo de Moura
f0c31d7e28 feat: allow rw to unfold nonrecursive definitions too 2022-03-12 15:44:52 -08:00
Leonardo de Moura
7af09ac009 refactor: move equation theorem cache to Meta/Eqns.lean 2022-03-12 15:34:32 -08:00
Leonardo de Moura
cf0ca026fb feat: equation theorems at rw 2022-03-12 13:53:02 -08:00
Leonardo de Moura
9d1dbada79 feat: only try to generate equation theorems for definitions whose types are not propositions 2022-03-12 13:44:33 -08:00
Leonardo de Moura
a6bfefe5bd fix: nasty performance problem at isDefEq 
This problem was originally exposed by the `Array.eraseIdxAux`.
 2022-03-12 10:44:43 -08:00
Leonardo de Moura
eddcedb58c fix: pattern normalization code 2022-03-12 06:07:04 -08:00
Lars
95cf18457d
chore: address review comments 2022-03-12 13:25:35 +00:00
Sebastian Ullrich
82c682d385 chore: remove redundant proof 2022-03-12 11:12:56 +01:00
Leonardo de Moura
a4f47adf9e fix: normalize method at Match.lean 2022-03-11 18:19:37 -08:00
larsk21
e430496903 doc: fix fuzzy matching docs 2022-03-11 16:25:26 -08:00
larsk21
ea5b6d568f fix: review suggestions + code structure 2022-03-11 16:25:26 -08:00
larsk21
0ef3ea4bc9 feat: enable fuzzy matching for workspace symbols 2022-03-11 16:25:26 -08:00
larsk21
64dba41b4c feat: enable fuzzy matching for completion 2022-03-11 16:25:26 -08:00
Sebastian Ullrich
ff11325fce perf: use mkArray in fuzzyMatchCore 2022-03-11 16:25:26 -08:00
Sebastian Ullrich
d48c5b99e9 perf: eliminate MProd allocations in iterateLookaround 2022-03-11 16:25:26 -08:00
Sebastian Ullrich
896b9b48a3 perf: eliminate some allocations in iterateLookaround 2022-03-11 16:25:26 -08:00
Sebastian Ullrich
7106d3fb34 perf: specialize iterateLookaround 2022-03-11 16:25:26 -08:00
larsk21
135eac71a1 feat: add string fuzzy matching 2022-03-11 16:25:26 -08:00
Leonardo de Moura
5caf1bc692 chore: style 
Use `·` instead of `.` for structuring tactics.
 2022-03-11 16:12:46 -08:00
Leonardo de Moura
ddf93d2f8a feat: support for arrow types in the dot notation 
cc @gebner
 2022-03-11 15:39:41 -08:00
Leonardo de Moura
8d42978e63 feat: generate error message when induction tactic is used on a nested inductive type without specifying an eliminator 2022-03-11 14:45:57 -08:00
Leonardo de Moura
7d5da95434 fix: remove unused hypotheses from conditional equation theorems 2022-03-11 14:10:57 -08:00
Leonardo de Moura
54b74796f6 feat: use tryContradiction at mkUnfoldProof 2022-03-11 12:52:15 -08:00
Leonardo de Moura
272dd5533f chore: style use · instead of . for lambda dot notation 
We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
 2022-03-11 07:49:03 -08:00
Leonardo de Moura
1b5e9c7c83 chore: use new notation on its own implementation 2022-03-10 16:56:39 -08:00
Leonardo de Moura
e1fa9c131c feat: inferring namespace from expected type a la Swift 
Now that `PatternVars.lean` has been redesigned, it is feasible to
implement issue #944.

closes #944
 2022-03-10 16:55:25 -08:00
Leonardo de Moura
1c99fe92ac feat: add dotIdent parser 
see #944
 2022-03-10 16:04:41 -08:00
Leonardo de Moura
3214a20d33 feat: allow overloaded notation in patterns 2022-03-10 12:51:34 -08:00
Leonardo de Moura
fddc8b06ac fix: missing case at getStuckMVar? 
Fix issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'rewrite'.20failed.20but.20it.20should.20work/near/274870747
 2022-03-10 10:33:11 -08:00
Leonardo de Moura
92318d07bb feat: add MonadBacktrack instance for CollectPatternVars.M monad 2022-03-10 10:23:18 -08:00
Leonardo de Moura
7a39be225d refactor: move methods to MetaM 2022-03-10 10:00:46 -08:00
Leonardo de Moura
2fb9a39cb4 refactor: implement MonadQuotation at CoreM 2022-03-10 09:55:20 -08:00
Leonardo de Moura
7850dc023b fix: make sure the structure instance notation does not leak auxiliary type annotations (e.g., autoParam and optParam) 2022-03-10 08:41:00 -08:00
Leonardo de Moura
efc89eb4e1 fix: make sure inferProjType consume auxiliary type annotations 2022-03-10 08:15:34 -08:00
Leonardo de Moura
0ef8aaeda0 feat: make sure minor premises in recursors do not include auxiliary type annotations (e.g., autoParam and optParam) 2022-03-10 08:08:36 -08:00
Leonardo de Moura
1afee372f7 refactor: move consume_type_annotations declaration to expr.h 2022-03-10 08:00:39 -08:00
Leonardo de Moura
33883e9d2a fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam) 2022-03-10 07:47:38 -08:00
Leonardo de Moura
5825eb394f refactor: move isOutParam to Expr.lean, rename consumeAutoOptParam => consumeTypeAnnotations 2022-03-10 07:37:41 -08:00
Leonardo de Moura
38668308ef fix: do not rename metavariables that are already in the patternVars array 
It fixes a regression introduced yesterday.
 2022-03-10 05:53:54 -08:00
Leonardo de Moura
9c5f6361a3 doc: document the new pattern elaboration procedure 2022-03-09 18:58:23 -08:00
Leonardo de Moura
ca253c43e1 refactor: pattern elaboration 
We don't use the following hack anymore:
-  /- HACK: `fvarId` is not in the scope of `mvarId`
-     If this generates problems in the future, we should update the metavariable declarations. -/
-  assignExprMVar mvarId (mkFVar fvarId)

This hack was corrupting the `InfoTree`.
 2022-03-09 18:19:14 -08:00
Leonardo de Moura
b0246172fa chore: add comment and remove dbg trace message 2022-03-09 14:02:30 -08:00
Leonardo de Moura
caa1366b62 fea: erase nested inaccessible annotations 2022-03-09 14:01:59 -08:00
Leonardo de Moura
1609f96128 refactor: simplify PatternVar.lean and Match.lean 2022-03-09 14:01:40 -08:00
Leonardo de Moura
74411aa472 fix: do not display implicit fields 2022-03-09 12:33:22 -08:00
Leonardo de Moura
50ae170bcc feat: allow mkLambdaFVars and mkForallFVars to abstract unassigned metavars too 2022-03-09 11:27:58 -08:00
Leonardo de Moura
4660485ac8 refactor: collectDeps => collectForwardDeps 2022-03-09 11:27:58 -08:00
Leonardo de Moura
5636c94cd0 chore: remove old comment, simplify exception 2022-03-09 11:27:58 -08:00