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
712e9b7d45
chore: add custom induction principle for LazyList
2022-03-11 14:21:35 -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
2364bc7b46
chore: add link to issue
2022-03-10 17:10:12 -08:00
Leonardo de Moura
002412e9d0
chore: missing code block annotation
2022-03-10 17:08:54 -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
61cd3dcc32
chore: update stage0
2022-03-10 16:55:40 -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
7a7841fa95
chore: update stage0
2022-03-10 16:07: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
3edb0ede04
chore: update stage0
2022-03-10 08:56:06 -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
c1b1a916eb
doc: update release notes
2022-03-10 08:26:27 -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
b6dc3dda04
chore: fix tests
2022-03-09 14:02:13 -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
Leonardo de Moura
1263cea6af
feat: add support for unassigned metavariables at dependsOn
2022-03-09 11:27:58 -08:00
Sebastian Ullrich
db9b963af7
chore: Nix: adjust message
2022-03-09 10:31:32 +01:00
Sebastian Ullrich
202258cc87
chore: Nix: remove debug flag
2022-03-09 10:30:37 +01:00
Sebastian Ullrich
a7438e9eae
chore: Nix: remove debug flag
2022-03-09 10:30:09 +01:00
Sebastian Ullrich
7821a201e9
chore: Nix: update Nix
2022-03-09 10:29:25 +01:00
Sebastian Ullrich
126c7dd4ea
chore: Nix: command for (one-time) linking .ileans
2022-03-09 10:29:25 +01:00
Sebastian Ullrich
2221cc8141
chore: Nix: emulate lake serve
2022-03-09 10:14:43 +01:00
Leonardo de Moura
164f07a5e5
feat: generalize Expr.abstractRange
...
It now takes free variables **and** metavariables.
This is the first step to make `mkForallFVars` and `mkLambdaFVars`
more general.
2022-03-08 18:19:17 -08:00
Leonardo de Moura
d6b782f811
chore: remove workaround
...
for regression introduced by the following change
* Auto implicit behavior changed for inductive families. An auto implicit argument occurring in inductive family index is also treated as an index (IF it is not fixed, see next item)
2022-03-08 17:58:20 -08:00
Leonardo de Moura
3b7ada0b35
chore: update stage0
2022-03-08 17:58:20 -08:00
Leonardo de Moura
4ee131981d
feat: in an inductive family the longest fixed prefix of indices is now promoted to parameters
...
This modification is relevant for fixing regressions on recent changes
to the auto implicit behavior for inductive families.
The following declarations are now accepted:
```lean
inductive HasType : Fin n → Vector Ty n → Ty → Type where
| stop : HasType 0 (ty :: ctx) ty
| pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty
inductive Sublist : List α → List α → Prop
| slnil : Sublist [] []
| cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
| cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
inductive Lst : Type u → Type u
| nil : Lst α
| cons : α → Lst α → Lst α
```
TODO: universe inference for `inductive` should be improved. The
current approach is not good enough when we have auto implicits.
TODO: allow implicit fixed indices that do not depend on indices that
cannot be moved to become parameters.
2022-03-08 17:56:34 -08:00
Leonardo de Moura
234046521a
feat: print number of parameters for an inductive type
2022-03-08 17:48:46 -08:00
Leonardo de Moura
7b84b4cdaa
fix: improve inductive indices elaboration
...
TODO: convert fixed indices to parameters. Motivation: types such as
```lean
inductive Foo : List α → Type
| mk : Foo []
```
Users should not need to write
```lean
inductive Foo {α} : List α → Type
| mk : Foo []
```
2022-03-08 17:48:46 -08:00
