Leonardo de Moura
ef154ec0cf
test: add TreeNode example using for in notation
2022-03-14 11:52:54 -07:00
Leonardo de Moura
cab3217b05
feat: add forIn'_eq_forIn theorem for lists
2022-03-14 11:50:47 -07:00
Leonardo de Moura
2ac9cfb7b1
fix: eta expand partial applications of recursive function being defined
2022-03-14 10:05:33 -07:00
Leonardo de Moura
801552e1ac
chore: fix tests
2022-03-14 10:05:33 -07:00
Leonardo de Moura
9988faf8bd
fix: missing mkRecAppWithSyntax
2022-03-14 10:05:33 -07:00
Leonardo de Moura
02145f66cf
chore: fix typo
2022-03-14 10:05:33 -07:00
Sebastian Ullrich
147a5c2933
chore: prefer LEAN_SRC_PATH
2022-03-14 17:24:25 +01:00
Leonardo de Moura
d2cc5b4a83
chore: fix test
2022-03-13 15:53:21 -07:00
Leonardo de Moura
fa0964c07e
fix: preserve variable name at WF decreasing goals when function has only one non fixed argument
2022-03-13 13:20:07 -07:00
Leonardo de Moura
060be7e7ec
fix: :: is infix right
2022-03-13 09:25:56 -07:00
Leonardo de Moura
672a889c83
test: add hlist pattern match example
2022-03-13 09:15:55 -07:00
Leonardo de Moura
30c153aa76
chore: update stage0
2022-03-12 20:18:20 -08:00
Leonardo de Moura
bfe57a1cb0
chore: simplify definition
2022-03-12 20:16:45 -08:00
Leonardo de Moura
231120c118
chore: update RELEASES.md
2022-03-12 20:02:39 -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
3cd41acd14
test: HList with notation overloads
2022-03-12 19:47:57 -08:00
Leonardo de Moura
af5a24140a
test: simple type checker at CPDT
2022-03-12 18:44:52 -08:00
Leonardo de Moura
7e3519a3a2
test: add CPDT first example
2022-03-12 17:06:20 -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
c0a72172f1
chore: update stage0
2022-03-12 15:35:09 -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
8a46668884
chore: update stage0
2022-03-12 10:46:17 -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
Leonardo de Moura
63dcf2124c
chore: add link to quickstart to README
2022-03-11 16:35:07 -08:00
Chris Lovett
6dc576121d
doc: replace quickstart leanpkg info with info about lake
2022-03-11 16:31:58 -08:00
Leonardo de Moura
15e30a93f3
feat: update RELEASES.md
2022-03-11 16:28:01 -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
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
