Daniel Fabian
93bb94bfea
test: update playground for Hashable
...
due to new code generation, adjust the playground code
2021-03-30 13:36:52 -07:00
Daniel Fabian
42c172eeec
feat: simplify Hashable implementation, allowing mutual recursive calls
...
change the generated to code recursively call the fields of recursive
and mutually recursive types. Currently, this can emit `partial`
functions due to lacking structural recursion. The code is prepared,
however, for the full implementation and can be trivially turned into
code generating non-`partial` functions
2021-03-30 13:36:52 -07:00
Daniel Fabian
ed75005422
feat: make proofs Hashable
...
change the `Hashable` class from taking a hash function of `Type u` to taking a
hash function from `Sort u`. This allows to implement `Hashable` for
propositions, which in turn is needed for inductives carrying proofs
2021-03-30 13:36:52 -07:00
Daniel Fabian
fee3390dd1
feat: add Hashable deriving
...
add support for the `Hashable` deriving by combining structural
hashes over fields
2021-03-30 13:36:52 -07:00
Leonardo de Moura
687ce2fe67
chore: update stage0
2021-03-30 13:32:06 -07:00
Leonardo de Moura
9f9529467e
chore: document recent modifications
2021-03-30 13:29:23 -07:00
Leonardo de Moura
b3a665118a
feat: add isAtomicDiscr?
2021-03-30 13:09:56 -07:00
Leonardo de Moura
4ec6804667
fix: issue at expandMatchAlts
2021-03-30 12:55:59 -07:00
Leonardo de Moura
19e0a84817
fix: make the match behavior more uniform
2021-03-30 12:19:31 -07:00
Sebastian Ullrich
7391e0ef92
fix: "unknown goal" on tactics nested in terms
2021-03-30 14:09:39 +02:00
Sebastian Ullrich
ac8f0526f6
feat: report goals from multiple info states
2021-03-30 11:38:34 +02:00
Sebastian Ullrich
06df67313c
refactor: goalsAt?
2021-03-30 11:27:42 +02:00
Leonardo de Moura
3db5b7e4ca
chore: remove dead code
2021-03-29 20:37:49 -07:00
Leonardo de Moura
f7d055830b
feat: save TacticInfo at ;
2021-03-29 20:31:48 -07:00
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
