Leonardo de Moura
745cff41db
feat: (try to) improve InfoTree.goalsAt? (yet another heuristic)
2021-03-29 19:30:00 -07:00
Leonardo de Moura
f75d9f50a6
feat: (try to) improve InfoTree.goalsAt?
2021-03-29 18:43:33 -07:00
Leonardo de Moura
913669f081
chore: add InfoTree.findInfo?
2021-03-29 17:08:47 -07:00
Leonardo de Moura
efe67453ac
chore: add Repr Lean.SourceInfo
2021-03-29 16:55:56 -07:00
Leonardo de Moura
564d0fe1cd
chore: add getHeadPos?
2021-03-29 16:55:29 -07:00
Leonardo de Moura
558ed3da90
fix: missing argument
...
cc @Kha
2021-03-29 16:55:10 -07:00
Leonardo de Moura
002f96adc1
test: discriminant refinement
2021-03-28 19:06:06 -07:00
Sebastian Ullrich
0dfefb7b78
fix: lean4-mode: inaccessibles highlighting
2021-03-28 17:56:28 +02:00
Sebastian Ullrich
9e3b8caa4b
feat: lean4-mode: show "goals accomplished"
2021-03-28 17:40:37 +02:00
Leonardo de Moura
f8adb449fe
fix: doc
2021-03-27 19:48:25 -07:00
Leonardo de Moura
c0407c7032
chore: update stage0
2021-03-27 19:44:33 -07:00
Leonardo de Moura
41539a7725
fix: leftovers in the local context when applying induction
2021-03-27 19:42:22 -07:00
Leonardo de Moura
566fad77d4
chore: helper methods
2021-03-27 18:48:03 -07:00
Leonardo de Moura
08d865b475
chore: remove unnecessary generalizing
2021-03-27 15:03:13 -07:00
Leonardo de Moura
aa753898c6
chore: update stage0
2021-03-27 15:00:39 -07:00
Leonardo de Moura
b32b542a85
chore: fix mkForbiddenSet
2021-03-27 14:59:05 -07:00
Leonardo de Moura
2e5a9d9c99
chor: fix import
2021-03-27 14:34:44 -07:00
Leonardo de Moura
4a0f8bf21a
feat: improve generalizing at induction
2021-03-27 14:28:03 -07:00
Leonardo de Moura
ba3d6103fa
chore: spaces
2021-03-27 14:07:45 -07:00
Leonardo de Moura
4705532231
chore: add missing instance
2021-03-27 14:06:33 -07:00
Leonardo de Moura
b899447817
refactor: move collectFVars to Meta
2021-03-26 19:16:21 -07:00
Leonardo de Moura
f20fc6328c
fix: better error message when cases fails and there are no alternatives
2021-03-26 16:28:21 -07:00
Leonardo de Moura
6cfc8d0937
fix: ensure discriminants are distinct variables
2021-03-26 16:28:21 -07:00
Leonardo de Moura
4a5368fd93
fix: accidental name capture
2021-03-26 16:28:21 -07:00
Sebastian Ullrich
2647cdf813
chore: fix trace.Elab.info position & redundancy
2021-03-26 11:39:44 +01:00
Sebastian Ullrich
170fc62c18
fix: tactic info post state
2021-03-26 11:25:52 +01:00
Sebastian Ullrich
8d543cbcdc
doc: using Nix with an external editor
2021-03-26 09:56:22 +01:00
Leonardo de Moura
a8d672f237
test: add Kevin and Yakov's examples
2021-03-25 17:22:14 -07:00
Leonardo de Moura
c79712becb
chore: fix test
2021-03-25 17:20:58 -07:00
Leonardo de Moura
81e986c11c
fix: intro with pattern
2021-03-25 17:19:17 -07:00
Leonardo de Moura
83b795b3b4
chore: update stage0
2021-03-25 16:51:00 -07:00
Leonardo de Moura
333646bc41
fix: add elabTermForApply
2021-03-25 16:50:37 -07:00
Leonardo de Moura
05022cc80b
fix: disable implicit lambda insertion at _, ?h, and by ...
...
@Kha This commit addresses an issue reported by Kevin. Holes and tactic
blocks represent a discontinuity in the elaboration process.
By introducing inaccessible variables (or "things" as Kevin calls
them), we create error message that are harder to understand (see
affected test), and goals where we didn't allow the user to select the
variable name and/or eagerly unfolded a definition.
BTW, I first considered using "reducible" setting when deciding
whether to insert implicit lambdas or not. This is a bad idea.
See `monotone.lean` test. The decision should not depend on
reducibility status, but whether there is "discontinuity" on the
elaboration process or not. As Kevin pointed out,
"introducing implicits work great if you finish the job".
2021-03-25 16:13:15 -07:00
Leonardo de Moura
dd9cc7a273
fix: typo
2021-03-25 15:57:10 -07:00
Leonardo de Moura
083301e286
fix: non-dependent arrow vs dependent arrow issue at DiscrTree
2021-03-25 13:04:24 -07:00
Leonardo de Moura
3bc26a64e6
chore: update stage0
2021-03-25 12:23:14 -07:00
Leonardo de Moura
b7acc38810
feat: add support for "arrow" at DiscrTree
2021-03-25 12:21:10 -07:00
Leonardo de Moura
59ac5be60d
chore: add ``
2021-03-25 12:21:10 -07:00
Sebastian Ullrich
1665f8d455
chore: Nix: update vscode-lean4
2021-03-25 18:53:44 +01:00
Sebastian Ullrich
3557d521d5
fix: don't unconditionally format InfoTrees in the server
2021-03-25 14:45:42 +01:00
Sebastian Ullrich
7b9ee8611c
fix: trace.Elab.Info in the server
2021-03-25 14:36:30 +01:00
Sebastian Ullrich
96c8cdfb14
chore: revert test changes
2021-03-25 10:35:22 +01:00
Leonardo de Moura
3176be136c
feat: improve "discriminant refinement"
2021-03-24 21:05:08 -07:00
Leonardo de Moura
ceba38526a
fix: save errToSorry
2021-03-24 20:54:14 -07:00
Leonardo de Moura
66a8683f08
fix: updateMatchType may generate type incorrect terms
...
If generated type is not correct, we should abort "discriminant
refinement", and use the original error message because users may
be confused by a type error on something they did not write.
2021-03-24 19:41:25 -07:00
Leonardo de Moura
f11a003526
test: add "discriminant refinement" tests
2021-03-24 19:10:50 -07:00
Leonardo de Moura
ce1dda8eea
fix: missing withMVarContext
2021-03-24 18:25:41 -07:00
Leonardo de Moura
ec5afce45b
feat: contextual := true at simp_all
...
cc @Kha
2021-03-24 15:49:31 -07:00
Leonardo de Moura
e4d4db45e9
feat: add missing simp lemmas for ->
2021-03-24 14:51:18 -07:00
Leonardo de Moura
4044308090
chore: use double quoted names
2021-03-24 12:36:18 -07:00
