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

8361 commits

Author SHA1 Message Date
Sebastian Ullrich
ed03ff9d00 perf: cache leading_parser and syntax as well 
We better hope the `leading_parser`s are closed terms
 2022-11-11 09:13:02 +01:00
Sebastian Ullrich
246923886a fix: do not create choice nodes for failed parses 2022-11-11 09:13:02 +01:00
Sebastian Ullrich
57320712f0 fix: extraneous missing items on parser stack 2022-11-11 09:13:02 +01:00
Leonardo de Moura
ca0fb21df4 fix: fixes #1813 
Remark: modifies the value for the `mid` priority.
See new note at `Init/Notation.lean`
 2022-11-10 16:09:21 -08:00
Leonardo de Moura
c147059fd7 fix: fixes #1812 2022-11-10 08:58:09 -08:00
Leonardo de Moura
7b8ade5ee4 test: String.get' and String.next' 2022-11-09 17:02:49 -08:00
Adrien Champion
1823735ebf chore: tests for strict-indent nested by-s 2022-11-08 08:30:42 -08:00
Mario Carneiro
4bf89dfa12 feat: allow doSeq in let x <- e | seq 
fixes #1804
 2022-11-08 08:29:21 -08:00
Leonardo de Moura
b4d13a8946 refactor: LetExpr => LetValue 
We use "let value" in many other places in the code base.
 2022-11-07 18:51:07 -08:00
Leonardo de Moura
d11697cbf7 chore: fix some tests 2022-11-07 18:18:06 -08:00
Mario Carneiro
4fefb2097f feat: hover/go-to-def/refs for options 2022-11-07 20:01:13 +01:00
Mario Carneiro
32b6bd0d8b feat: empty type ascription syntax (e :) (part 2) 2022-11-07 19:10:56 +01:00
Alex J Best
8da48f2381 chore: typo fix in error message of overlapping structure fields 2022-11-05 12:41:40 -07:00
Scott Morrison
d0dc9a2f90
fix: reorder goals after specialize (#1796) 
* fix: reorder goals after specialize

* fix test
 2022-11-03 06:32:55 -07:00
Mario Carneiro
9b40613207 fix: formatting for if let and do if 2022-11-01 20:19:39 -07:00
Mario Carneiro
ad1c23f172 fix: bug in replaceLocalDeclDefEq 
fixes #1615
 2022-11-01 19:18:25 -07:00
Sebastian Ullrich
9b05f57ec8 fix: wrap &"..." <|> ... as well 2022-10-28 21:25:47 +02:00
Sebastian Ullrich
731e28df00 fix: syntax match should not ignore tokens in <|> 2022-10-28 21:25:47 +02:00
Leonardo de Moura
5f38a483f2 fix: congr tactic 
`MVarId.congr?` and `MVarId.hcongr?` should return `none` if an
exception is thrown while applying congruence theorem.

`MVarId.hcongr?` should try `eq_of_heq` before trying to apply
`hcongr` theorem.

closes #1787

BTW: Lean 4 `congr` tactic is applying `assumption`. Lean 3 version does not.
 2022-10-28 08:00:04 -07:00
Leonardo de Moura
31d2c8fb66 chore: fix test 2022-10-27 18:57:25 -07:00
Leonardo de Moura
ad98df80fe feat: congr theorems using Iff 
closes #1763
 2022-10-26 18:00:24 -07:00
Leonardo de Moura
5e25d9148a feat: improve apply error message when root term elaboration is postponed 
fixes #1719
 2022-10-26 17:15:24 -07:00
Leonardo de Moura
0b6b754bca feat: improve apply tactic 
It tries to address what the Mathlib community calls the "apply bug".

cc @digama0
 2022-10-26 16:58:43 -07:00
Leonardo de Moura
f3b1eadb55 feat: copy docstring when copying parent fields 
closes #1730
 2022-10-26 15:43:46 -07:00
Leonardo de Moura
83d8e36773 fix: fixes #1780 2022-10-26 07:46:38 -07:00
Leonardo de Moura
5a8f9ace72 fix: open .. hinding .. should activate scoped attributes 2022-10-26 07:39:06 -07:00
Leonardo de Moura
e369c3beb6 fix: disallow . immediately after .. 
Rejects the following weird example
```
```
which was being parsed as
```
```
 2022-10-26 07:13:40 -07:00
Leonardo de Moura
d7e732e886 feat: use unop% to implement unary minus notation 
closes #1779
 2022-10-26 06:55:24 -07:00
Mario Carneiro
a086d217a5 fix: bug in level normalization (soundness bug) 2022-10-26 05:22:26 -07:00
Sebastian Ullrich
1893857f15 fix: expandCDot? should create canonical syntax 2022-10-25 12:23:13 +02:00
Sebastian Ullrich
f39281f6b4 fix: hoverableInfoAt? in presence of canonical syntax 2022-10-25 12:23:13 +02:00
Gabriel Ebner
725aa8b39a refactor: instantiateTypeLevelParams in Lean 2022-10-24 12:23:13 -07:00
Yuri de Wit
c98b3a5388 fix: add local Hashable instance (fixes #1737) 
When inductives are indirectly mutually recursive, say `inductive T | t
(args: List T)` instead of `inductive T | t (arg : T)`, Lean would fail
to find an instance of Hashable for `T` because it was not yet defined.

This commit makes sure that the deriving handler adds a needed Hashable T
instance to the local scope so that Hashable.hash can be resolved
recursively.
 2022-10-23 21:26:04 +02:00
Mario Carneiro
c4cbefce11 feat: add linter.deprecated option to silence deprecation warnings 2022-10-23 21:11:57 +02:00
Gabriel Ebner
fc304d95c0 feat: Min/Max typeclasses 2022-10-21 14:36:38 -07:00
E.W.Ayers
112cb5e261 test: fix test output 2022-10-20 11:20:42 -07:00
E.W.Ayers
c9a26596dc refactor: switch resolve to double eval strategy 
Using option (2) from this comment:
https://github.com/leanprover/lean4/pull/1661#pullrequestreview-1135363727
 2022-10-20 11:20:42 -07:00
E.W.Ayers
691835037e feat: code action resolvers 2022-10-20 11:20:42 -07:00
E.W.Ayers
297d06fc0c fix: issue where code action was not running 2022-10-20 11:20:42 -07:00
E.W.Ayers
8085ce88e9 feat: CodeActionProvider 
This is a low-level system for registering LSP code actions.
Developers can register their own code actions.
In future commits I am going to add features on top of this.
 2022-10-20 11:20:42 -07:00
Leonardo de Moura
aeddcbdc6d fix: disable implicit lambdas at intro <pattern> notation 
See issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/intro.20with.20type.20specified/near/305150215
 2022-10-20 09:04:06 -07:00
Mario Carneiro
dd8bbe9367 fix: catch kernel exceptions in Kernel.{isDefEq, whnf} 
fixes #1756
 2022-10-20 05:38:29 -07:00
Mario Carneiro
583e023314 chore: snake-case attributes (part 2) 2022-10-19 09:28:08 -07:00
Mario Carneiro
dd5948d641 chore: snake-case attributes (part 1) 2022-10-19 09:28:08 -07:00
Sebastian Ullrich
9fd433785b chore: register pretty printer trace classes 2022-10-19 14:51:07 +02:00
Gabriel Ebner
0c2a5580cb feat: enforce correct syntax kind in macros 2022-10-18 14:59:14 -07:00
Gabriel Ebner
fb4d90a58b feat: dynamic quotations for categories 2022-10-18 14:59:14 -07:00
Leonardo de Moura
ec59bbe15c chore: ensure LCNF pretty printer result supports Format.group 2022-10-16 16:06:08 -07:00
Leonardo de Moura
72c576f62a feat: complete reduceArity pass 2022-10-16 16:00:33 -07:00
Leonardo de Moura
1a02c326e5 chore: fix test 2022-10-16 14:54:07 -07:00