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

185 commits

Author SHA1 Message Date
Leonardo de Moura
3e7d45aaba fix: improve finer-grained term infos for do blocks 
see #1248

This commit adds a small hack to fix the term info for the following `do`-elements
```lean
   let (x, y) := ...
   let (x, y) ← ...
   let mut (x, y) ← ...
   let some x ← ... | ...
```
 2022-07-26 18:18:05 -07:00
Leonardo de Moura
0e3f031660 fix: position information for with_annotate_term when coercions are used 
see #1248
 2022-07-26 16:09:45 -07:00
Leonardo de Moura
c22120371e feat: finer-grained term infos for do blocks 
closes #1248
 2022-07-26 15:47:37 -07:00
Leonardo de Moura
28fc2f9d37 fix: improve "{varName} cannot be reassigned" error message 
closes #1341
 2022-07-24 07:44:34 -07:00
Leonardo de Moura
ad5ee05a03 chore: consistent use of backticks in error messages at Do.lean 2022-07-24 07:42:04 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! (#1354) 2022-07-22 12:05:31 -07:00
Gabriel Ebner
a8cab84735 refactor: use computed fields for Expr 2022-07-11 14:19:41 -07:00
Leonardo de Moura
e4b358a01e refactor: prepare to elaborate a[i] notation using typeclasses 2022-07-09 15:24:22 -07:00
Leonardo de Moura
bdaabd4e7b feat: propagate return type to for-in block 2022-07-08 17:29:30 -07:00
Leonardo de Moura
7cf31f7360 chore: update comment 2022-07-08 15:34:09 -07:00
Sebastian Ullrich
d7bcc271be refactor: avoid nested sequence in simpleBinder 2022-07-08 19:06:10 +02:00
Leonardo de Moura
71550c55a9 fix: @ scope 2022-07-06 19:42:43 -07:00
Leonardo de Moura
f8c7bd71aa fix: position information for toStream application at do-notation 2022-07-06 18:50:45 -07:00
Leonardo de Moura
645c3e777d feat: disable coeAtOutParam when @ (aka explicit = true) is used 2022-07-06 18:31:39 -07:00
Leonardo de Moura
2ebcf29cde chore: use a[i]! for array accesses that may panic 2022-07-02 15:12:05 -07:00
Leonardo de Moura
d83a11bac5 chore: expose exprToSyntax 2022-06-29 16:02:01 -07:00
Leonardo de Moura
e968dfb68c feat: elaborate do notation even when expected type is not available 
see issue #1256
 2022-06-29 13:30:06 -07:00
Sebastian Ullrich
22475b8669 refactor: introduce common TSyntax abbreviations 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
d9cfda4893 refactor: make more use of quotations 
Automatically fixes many TSyntax type errors
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
5e334b3e90 chore: postpone TSyntax adoption for some parts 
The namespace `TSyntax.Compat` can be opened for a coercion
`Syntax -> TSyntax k` for any `k`, as otherwise this PR would never be done.
 2022-06-27 22:37:02 +02:00
Leonardo de Moura
77ae79be46 chore: use let/if in do blocks 2022-06-13 17:10:14 -07:00
Sebastian Ullrich
61232e788a fix: check types at do pattern reassignment 2022-06-10 17:31:36 +02:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
Leonardo de Moura
dca8a8ed98 fix: match or-pattern 
This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Probably.20a.20bug/near/283779934
 2022-05-25 20:05:46 -07:00
Leonardo de Moura
f44a701637 chore: style 2022-05-11 15:32:18 -07:00
Sebastian Ullrich
91991649bc fix: connect occurrences of mutable variable inside and outside for in info tree 2022-05-07 15:50:26 -07:00
Sebastian Ullrich
22f8ea147c fix: propagate position information of variables in do blocks 2022-05-07 15:50:26 -07:00
Leonardo de Moura
6d926c7989 feat: macro expand match alternatives 
see #371

This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
  | S (s : String)
  | I (i : Int)

def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a => toString a
  | S a => toString a
```
 2022-03-20 14:20:13 -07:00
Leonardo de Moura
8f4d58893f feat: update match parser 
Support for
```
def fib (x : Nat) : Nat :=
  match x with
  | 0 | 1 => 1
  | x+2   => fib (x+1) + fib x
```

TODO: expand `matchAlts`
 2022-03-20 13:22:39 -07:00
Leonardo de Moura
8b248e2d8c feat: elaborate for h : x in xs do ... notation 2022-03-03 19:52:26 -08:00
Leonardo de Moura
92937b3aba feat: add for h : x in xs do ... notation 
The idea is to have `h : x \in xs`.
This commit just adds the parser.
 2022-03-03 18:27:40 -08:00
Leonardo de Moura
93b5b74b36 feat: modify notation for providing motive in "match" expressions 2022-02-14 15:36:14 -08:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Leonardo de Moura
5f74cd4968 feat: add let pat := val | elseCase do-notation 2022-02-03 15:55:03 -08:00
Mario Carneiro
5e36162f9b fix: adapt to doHave syntax change 2022-01-03 07:55:52 -08:00
Leonardo de Moura
3856d0030c feat: improve do notation error message for pure code 
See #770
 2021-12-13 11:08:38 -08:00
Leonardo de Moura
483f32edd8 feat: in pure code, do use assume Id monad at do notation 
This feature produced counterintuitive behavior and confused users.
See discussion at #770.

As pointed out by @tydeu, it is not too much work to write `Id.run <|`
before the `do` when we want to use the `do` notation in pure code.

closes #770
 2021-12-10 12:55:14 -08:00
Gabriel Ebner
bfc74decde feat: add info field to Syntax.node 2021-10-26 20:19:27 +02:00
Siddharth Bhat
3374806d0f refactor: eliminate unused ExtractMonadResult.hasBindInst 2021-10-15 06:57:24 -07:00
Leonardo de Moura
acd21052c0 chore: remove old notation 2021-10-02 15:06:40 -07:00
Leonardo de Moura
b99f1c698b feat: use if-then-else notation at Do.lean 
Otherwise, the `if` in the `Do` notation will not benefit from the
improved elaborator.
 2021-09-30 22:34:36 -07:00
Leonardo de Moura
d378df47d7 fix: fixes #633 2021-09-16 14:11:34 -07:00
Leonardo de Moura
a821dcbff2 chore: enforce naming convention for theorems 
see issue #402

fix: `ElabTerm.lean`
 2021-08-07 12:48:38 -07:00
Leonardo de Moura
76cc99179d fix: fixes #370 2021-08-06 12:52:23 -07:00
Sebastian Ullrich
4a4b4c1ef4 fix: mkAtomFrom: generate synthetic position like other *From functions 
Also consistently use binders as reference position for an elided binder type.
Before, type errors were always given extent 1, the length of the
synthetic `_` token.
 2021-07-19 13:24:59 -07:00
Leonardo de Moura
953dd85c06 chore: avoid inline 2021-06-28 10:17:01 -07:00
Leonardo de Moura
ae6a28af52 chore: remove unnecessary specialize 2021-06-28 10:11:23 -07:00
Leonardo de Moura
712206f80e refactor: add BindersUtil.lean 2021-06-28 08:44:16 -07:00
Leonardo de Moura
7e1bb3e65b refactor: add MatchAltView.lean and PatternVar.lean 2021-06-28 08:29:47 -07:00