Leonardo de Moura
|
ef8fecff79
|
feat: add Level.geq
|
2022-04-03 08:18:14 -07:00 |
|
Leonardo de Moura
|
310961cc35
|
chore: add scaffolding for checking ctor universe params
|
2022-04-03 07:33:02 -07:00 |
|
Leonardo de Moura
|
743f6dd3a2
|
chore: cleanup
|
2022-04-03 06:56:27 -07:00 |
|
Leonardo de Moura
|
ca9b494e4d
|
chore: use specialize tactic
|
2022-04-02 19:35:36 -07:00 |
|
Leonardo de Moura
|
d7abecd07d
|
test: addDecorations without partial
|
2022-04-02 19:08:21 -07:00 |
|
Leonardo de Moura
|
c873ad6ef3
|
test: recursive function on Syntax without partial
|
2022-04-02 18:43:45 -07:00 |
|
Leonardo de Moura
|
9d55d7bf9e
|
feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs
|
2022-04-02 18:38:55 -07:00 |
|
Leonardo de Moura
|
64cfbc1ae3
|
feat: add helper tactic for applying sizeOf (a.get i) < sizeOf a automatically in termination proofs
|
2022-04-02 18:29:41 -07:00 |
|
Leonardo de Moura
|
562af50191
|
feat: add ForIn' instance for Range
|
2022-04-02 18:22:21 -07:00 |
|
Leonardo de Moura
|
2c7c7471db
|
feat: add case' tactic for writing macros
It is similar to `case` but does not admit goal in case of failure.
This is useful for writing macros.
|
2022-04-02 17:54:06 -07:00 |
|
Leonardo de Moura
|
443dd79a02
|
feat: sizeOf theorems for Lean.Name
|
2022-04-02 17:09:55 -07:00 |
|
Leonardo de Moura
|
03ec8cb30b
|
feat: missing sizeOf theorems for Array.get and List.get
|
2022-04-02 16:04:46 -07:00 |
|
Leonardo de Moura
|
9f29d7ecb7
|
feat: add stop tactic macro
|
2022-04-02 15:39:03 -07:00 |
|
Leonardo de Moura
|
3d4e6282b7
|
chore: fix link to examples
|
2022-04-02 15:29:12 -07:00 |
|
Leonardo de Moura
|
78007be772
|
test: for Lean 3 hover issue reported on Zulip
|
2022-04-02 15:21:24 -07:00 |
|
Leonardo de Moura
|
4fa5f50559
|
feat: implement TODO at "fixed indices to parameters"
The missing feature (TODO in the code) is needed for the `BinTree` example.
|
2022-04-02 14:37:24 -07:00 |
|
Leonardo de Moura
|
9fe5458077
|
feat: do not display inaccessible proposition names if they do not have forward dependencies
Even if `pp.inaccessibleNames = true`
|
2022-04-02 13:15:17 -07:00 |
|
Leonardo de Moura
|
95bd55bc21
|
chore: fix typo and remove unnecessary discriminant
|
2022-04-02 13:15:17 -07:00 |
|
Sebastian Ullrich
|
4fcc7c78dd
|
chore: update LeanInk
|
2022-04-02 18:13:42 +02:00 |
|
Leonardo de Moura
|
d65ceafc99
|
chore: break long lines
|
2022-04-02 07:54:40 -07:00 |
|
Leonardo de Moura
|
9ee3cb642a
|
chore: formatting
|
2022-04-02 07:53:20 -07:00 |
|
Leonardo de Moura
|
e4fb9c8f47
|
chore: break long lines
|
2022-04-02 07:50:27 -07:00 |
|
Leonardo de Moura
|
375692cb92
|
doc: explain attribute [local simp]
|
2022-04-02 07:46:32 -07:00 |
|
Leonardo de Moura
|
16649beb19
|
doc: explain details
|
2022-04-02 07:39:07 -07:00 |
|
Leonardo de Moura
|
dee5dbca98
|
chore: cleanup example
|
2022-04-02 07:13:46 -07:00 |
|
Leonardo de Moura
|
7f00352d33
|
chore: backtick issue in documentation
|
2022-04-02 06:55:23 -07:00 |
|
Leonardo de Moura
|
e058fe65a9
|
feat: make the hypothesis name optional in the by_cases tactic
|
2022-04-01 19:36:13 -07:00 |
|
Leonardo de Moura
|
ed935ed7a7
|
doc: binary search trees
|
2022-04-01 19:30:28 -07:00 |
|
Leonardo de Moura
|
8636594dac
|
chore: add [simp] to Nat.lt_irrefl
|
2022-04-01 18:50:32 -07:00 |
|
Leonardo de Moura
|
be014b1fc9
|
fix: dotted notation corner case
|
2022-04-01 18:20:44 -07:00 |
|
Leonardo de Moura
|
cfb4e306f7
|
refactor: replace length_dropLast theorem
|
2022-04-01 16:44:24 -07:00 |
|
Leonardo de Moura
|
2ec40e91da
|
chore: update stage0
|
2022-04-01 15:48:09 -07:00 |
|
Leonardo de Moura
|
a926cd1698
|
fix: mkUnfoldProof
The hypotheses in an equation theorem may depend on each other
|
2022-04-01 15:47:24 -07:00 |
|
Leonardo de Moura
|
4a0f68de83
|
fix: split tactic issue
|
2022-04-01 15:47:24 -07:00 |
|
Leonardo de Moura
|
ea8f31144e
|
feat: add predicate to generalize tactic to select subterms to be generalized
|
2022-04-01 15:47:24 -07:00 |
|
Sebastian Ullrich
|
524dc5d47c
|
chore: Nix: update Nixpkgs
|
2022-04-02 00:08:24 +02:00 |
|
Leonardo de Moura
|
d473cc5a4c
|
chore: update release notes for issue #1090
closes #1090
|
2022-04-01 11:38:50 -07:00 |
|
Leonardo de Moura
|
0241d7c197
|
chore: fix tests
|
2022-04-01 11:34:50 -07:00 |
|
Leonardo de Moura
|
f45712ce74
|
chore: update stage0
|
2022-04-01 11:29:09 -07:00 |
|
Leonardo de Moura
|
fdd1cb5751
|
chore: remove workarounds for #1090
|
2022-04-01 11:28:17 -07:00 |
|
Leonardo de Moura
|
48a3668780
|
chore: fix repo
|
2022-04-01 11:24:30 -07:00 |
|
Leonardo de Moura
|
16b2237d2d
|
chore: update stage0
|
2022-04-01 11:24:22 -07:00 |
|
Leonardo de Moura
|
799c701f56
|
fix: inconsistency between syntax and kind names
TODO: remove staging workarounds
see #1090
|
2022-04-01 11:20:16 -07:00 |
|
Leonardo de Moura
|
b6cc3c959b
|
chore: update stage0
|
2022-04-01 11:14:47 -07:00 |
|
Leonardo de Moura
|
68acfc7fb9
|
chore: prepare for #1090
|
2022-04-01 11:11:28 -07:00 |
|
Leonardo de Moura
|
8dddb0ddc7
|
chore: update stage0
|
2022-04-01 09:37:52 -07:00 |
|
Leonardo de Moura
|
09de67780f
|
chore: prepare for #1090
|
2022-04-01 09:35:06 -07:00 |
|
Leonardo de Moura
|
414f5596a6
|
test: Nat.binrec example
|
2022-04-01 08:29:44 -07:00 |
|
Leonardo de Moura
|
d1022e5587
|
chore: add Nat.div_add_mod
|
2022-04-01 08:20:00 -07:00 |
|
Leonardo de Moura
|
92382ea47b
|
fix: checkpoint
|
2022-04-01 05:53:18 -07:00 |
|