max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
23926 commits 1 branch 0 tags 5.3 GiB
Commit graph

514 commits

Author SHA1 Message Date
Leonardo de Moura
5f80659b45 fix: unfold constants at simp 2021-02-16 15:42:31 -08:00
Leonardo de Moura
3e65f586cc fix: smart unfolding 2021-02-16 15:39:07 -08:00
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
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
7bdd3ae5a2 feat: simplify ctor_1 ... = ctor_2 ... 2021-02-15 12:40:19 -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
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
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
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
Leonardo de Moura
9ba8a30fb2 feat: add Repr instance for CongrLemmas 2021-02-11 18:13:33 -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
83775b08cb fix: whnfCore not expanding delayed assignments 2021-02-05 15:14:12 -08:00
Leonardo de Moura
4dc2a84302 fix: whnfCore 
Update function before invoking `reduceMatcher?`
 2021-02-05 13:40:39 -08:00
Leonardo de Moura
cab3c72374 fix: isDefEq for applications in WHNF 
The issue fixed by this commit was exposed by c17a1c382f
We also document the TC workaround used at `tryHeuristic`.
 2021-02-05 12:42:34 -08:00
Leonardo de Moura
c17a1c382f fix: isDeltaCandidate? 
It should return `some ...` only if `ConstantInfo` has a value.
 2021-02-05 09:19:37 -08:00
Leonardo de Moura
278d47c772 chore: add Repr instance for TransparencyMode 2021-02-04 20:40:05 -08:00
Leonardo de Moura
e415cfa632 chore: increase synthInstance.maxHeartbeats default 2021-02-04 17:36:12 -08:00
Leonardo de Moura
c747230e28 refactor: move isMonad? to AppBuilder.lean 2021-02-04 17:17:51 -08:00
Leonardo de Moura
e63111b39a fix: fixes #302 
TODO: investigage error message duplication
 2021-02-03 15:04:18 -08:00
Leonardo de Moura
2888e49785 feat: @ modifier at induction and cases tactic alternatives 2021-02-01 18:03:19 -08:00
Leonardo de Moura
c1dce595a5 feat: add option useNamesForExplicitOnly to introN 2021-02-01 17:35:48 -08:00
Leonardo de Moura
b4dfa08543 chore: store eliminator name at ElimInfo 2021-02-01 13:16:52 -08:00
Leonardo de Moura
b7a0bdb9c9 fix: Injection.lean 2021-01-30 11:58:56 -08:00
Leonardo de Moura
a58ff18a5b refactor: pos at time_task::time_task was a dead field 2021-01-30 11:10:18 -08:00
Leonardo de Moura
761b64c929 fix: missing occursCheck at SyntheticMVars 
fixes #301
 2021-01-29 17:13:04 -08:00
Leonardo de Moura
bf77f0707e refactor: remove no-mutual workaround 
This is still leftover from the old frontend.
 2021-01-29 17:13:04 -08:00
Leonardo de Moura
920ae5f1b9 chore: cleanup 2021-01-29 17:13:04 -08:00
Leonardo de Moura
e102cd4f42 fix: checkAssignment must be at assignConst 
Example of issue fixed by this commit: the variables `xs` may have references to `mvar`.
 2021-01-29 17:13:03 -08:00
Leonardo de Moura
8699f439da chore: avoid big match-expr 2021-01-29 17:13:03 -08:00
Leonardo de Moura
27a27d33d2 feat: special cases for mkCongrArg, mkCongrFun, mkCongr 2021-01-28 12:19:56 -08:00
Leonardo de Moura
1d76f3e1c1 chore: cleanup 2021-01-28 12:03:06 -08:00
Leonardo de Moura
70d6ea57a2 fix: mkSizeOfSpecLemmaInstance 
It was not handling correctly constructors with implicit fields.
 2021-01-27 18:24:32 -08:00
Leonardo de Moura
f1a0044241 fix: use previously generated sizeOf_spec lemmas to expand rhs 2021-01-27 18:14:25 -08:00
Leonardo de Moura
c47c25cf33 feat: finish sizeOf_spec lemma generation 2021-01-27 17:20:23 -08:00
Leonardo de Moura
7d4f80fbc6 chore: fix name 2021-01-27 16:26:34 -08:00
Leonardo de Moura
992e0c5ded feat: auxiliary sizeOf lemma recursor skeleton 
TODO: minor premises
 2021-01-27 16:18:53 -08:00
Leonardo de Moura
afdc19c2f1 feat: generalize indices at mkSizeOfAuxLemma 2021-01-27 15:16:43 -08:00
Leonardo de Moura
6c119a1921 chore: use register_builtin_option 2021-01-26 18:24:56 -08:00
Leonardo de Moura
4fc2aead45 fix: missing checkAssignment at assignToConstFun 
Fixes #297
 2021-01-26 17:33:33 -08:00
Leonardo de Moura
4ed43bd925 chore: cleanup 2021-01-26 17:16:10 -08:00
Leonardo de Moura
2c05e78728 fix: bug at CheckAssignment 2021-01-26 16:20:41 -08:00