Leonardo de Moura
4ec85a39a5
fix: Not should not be reducible, special support for Ne
...
Unification hint for `Not`
2021-02-15 17:36:11 -08:00
Leonardo de Moura
242a8dcfbf
test: simp
2021-02-15 17:09:51 -08:00
Leonardo de Moura
99ba21a881
chore: annotations for simp
2021-02-15 17:04:47 -08:00
Leonardo de Moura
e97df2f61b
feat: functions to unfold at simp
2021-02-15 15:32:25 -08:00
Leonardo de Moura
1c5de9842d
feat: use decide at simp
2021-02-15 13:08:45 -08:00
Leonardo de Moura
51bdf670fa
chore: add simp helper lemmas
2021-02-15 12:42:13 -08:00
Leonardo de Moura
7bdd3ae5a2
feat: simplify ctor_1 ... = ctor_2 ...
2021-02-15 12:40:19 -08:00
Leonardo de Moura
9528c1abd7
chore: add basic simp lemmas
...
TODO: consistent naming convention for theorems.
cc @Kha
2021-02-15 11:32:19 -08:00
Leonardo de Moura
3bc5b89ac3
test: add if p x then .. else .. example
...
cc @Kha
2021-02-14 11:44:10 -08:00
Leonardo de Moura
1106145ee7
chore: update stage0
2021-02-14 11:36:08 -08:00
Leonardo de Moura
ac51d3e621
feat: eager coe expansion
2021-02-14 11:34:08 -08:00
Leonardo de Moura
f07b9926b1
feat: unfold coercions and coeFun, coeSort, coeM, liftCoeM
...
TODO: `coe`
2021-02-14 10:27:34 -08:00
Leonardo de Moura
7e3bc30674
feat: add expandCoe
2021-02-14 10:03:44 -08:00
Leonardo de Moura
0787886cea
feat: improve simp local lemma elaboration
2021-02-13 18:55:19 -08:00
Leonardo de Moura
2944da2a0b
feat: use simp itself as default method for discharging hypotheses of conditional rewriting rules
2021-02-13 18:55:19 -08:00
Leonardo de Moura
3a9cd7e85b
refactor: use Simp.Context instead of Config+SimpLemmas+CongrLemmas
2021-02-13 18:55:19 -08:00
Leonardo de Moura
1a4eaa2418
chore: arguments occurring in the lhs should be marked as implicit
2021-02-13 18:55:19 -08:00
Sebastian Ullrich
95183e4e60
chore: Nix: update vscode-lean4 to 0.0.6
2021-02-13 16:42:21 +01:00
Leonardo de Moura
21878030d1
fix: fixes #310
...
@Kha I implemented the following approach:
- Error if user tries to revert `auxDecl`.
- Clear any `auxDecl` that depends on variables being reverted by the user.
2021-02-12 18:14:42 -08:00
Sebastian Ullrich
75243e7f24
feat: change back seqLeft/Right signature
...
This was originally changed for the sake of `do`, which does not depend on it anymore
2021-02-12 17:08:06 -08:00
Leonardo de Moura
c64d053f9e
test: ite and dite congr test
2021-02-12 16:52:56 -08:00
Leonardo de Moura
4ac78266ad
fix: make sure temporary metavars don't leak
2021-02-12 16:52:56 -08:00
Leonardo de Moura
1945858d89
fix: assigned metavariables in SimpLemmas
2021-02-12 16:52:56 -08:00
Leonardo de Moura
16a6778fb6
fix: avoid nonstandard instances at ite and dite congruence lemmas
...
cc @gebner
2021-02-12 16:52:56 -08:00
Leonardo de Moura
b51e3cb1fe
feat: process congr lemmas at simp
2021-02-12 16:52:56 -08:00
Leonardo de Moura
da91fc4526
refactor: move synthesizeArgs
2021-02-12 16:52:56 -08:00
Sebastian Ullrich
172d47c468
chore: CI: fix
2021-02-12 22:55:22 +01:00
Sebastian Ullrich
5db8073c32
chore: CI: nightlies race condition
2021-02-12 22:16:52 +01:00
Leonardo de Moura
9ba8a30fb2
feat: add Repr instance for CongrLemmas
2021-02-11 18:13:33 -08:00
Leonardo de Moura
3a66dbf0fd
chore: annotate ite/dite congruence lemmas
2021-02-11 17:55:42 -08:00
Leonardo de Moura
88c1b7fc99
chore: update stage0
2021-02-11 17:53:25 -08:00
Leonardo de Moura
ffa4a577be
feat: add @[congr] attribute
2021-02-11 17:51:04 -08:00
Leonardo de Moura
8b3c61dbb0
fix: checkAssignment
2021-02-11 16:56:32 -08:00
Leonardo de Moura
5e0b6a404f
chore: naming convention
2021-02-11 15:05:26 -08:00
Leonardo de Moura
c0f5ab1fa5
feat: add congruence lemmas for simp
2021-02-11 14:07:01 -08:00
Sebastian Ullrich
18aaef4d93
chore: fix test
2021-02-11 18:45:06 +01:00
Sebastian Ullrich
8320ab6177
fix: syntax match: check identifiers (using strict equality)
2021-02-11 17:50:05 +01:00
Sebastian Ullrich
19306a844f
chore: delaborator: print BinderInfo.auxDecl as explicit
2021-02-11 12:13:22 +01:00
Sebastian Ullrich
10bcd0bc9e
fix: #check_failure
2021-02-11 11:30:37 +01:00
Sebastian Ullrich
a74960a4ab
fix: delaborator: match with shadowing
2021-02-11 11:30:25 +01:00
Leonardo de Moura
896ce41b33
chore: fix test
2021-02-10 12:04:33 -08:00
Leonardo de Moura
8815e76b4d
chore: update stage0
2021-02-10 09:59:55 -08:00
Leonardo de Moura
12fb6be170
chore: update stage0
2021-02-10 09:56:14 -08:00
Leonardo de Moura
2aed9a4ec2
chore: special support for match d with | PUnit.unit => rhs
2021-02-10 09:54:12 -08:00
Leonardo de Moura
16429e393d
test: add dep hd test
...
It has been reported in the general channel that this example
generates problems for the Lean 3 elaborator.
2021-02-08 11:26:23 -08:00
Sebastian Ullrich
f7e5fec4d1
feat: lean4-mode: add more suffix characters to word category
2021-02-07 18:27:55 +01:00
Sebastian Ullrich
8b1d02c083
feat: lean4-mode: highlight inaccessible names in goal display using font-lock-comment-face
2021-02-07 18:27:55 +01:00
Leonardo de Moura
be10f35a8d
chore: update stage0
2021-02-06 18:00:29 -08:00
Leonardo de Moura
4e4194af41
feat: add autoBoundImplicit support for structure fields
2021-02-06 17:58:29 -08:00
Leonardo de Moura
023d7605fb
feat: add "transitivity" to "has_loose_bvars_in_domain"
2021-02-06 17:42:38 -08:00
