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

4033 commits

Author SHA1 Message Date
Leonardo de Moura
126ad49401 feat: add stage1 extension for storing LCNF declarations 2022-08-14 10:59:36 -07:00
Leonardo de Moura
745f77c657 chore: let x := lcUnreachable .. should not occur in LCNF 2022-08-13 16:24:44 -07:00
Leonardo de Moura
6c5638d85b fix: bug at toLCNF 2022-08-13 15:22:22 -07:00
Leonardo de Moura
7b440040f8 test: add Gabriel's examples 
They expose issues in the current code generator
 2022-08-13 11:51:09 -07:00
Leonardo de Moura
cba5f1b374 test: add examples that produce the LCNF "any" type 2022-08-13 11:37:35 -07:00
Leonardo de Moura
0b585d6f3d fix: bug at Compiler/Check.lean 2022-08-12 13:59:56 -07:00
Leonardo de Moura
37057fdd31 feat: eagerly inline simple join points 2022-08-12 11:15:12 -07:00
Leonardo de Moura
cfbefd993b fix: lambdaBoundedTelescope at Compiler/Check.lean 2022-08-12 10:20:54 -07:00
Leonardo de Moura
104196e599 feat: add profileitM to compiler new entry point 2022-08-11 19:04:33 -07:00
Leonardo de Moura
6d5272a404 fix: new compiler type checker 2022-08-11 18:57:06 -07:00
Leonardo de Moura
2eab711308 chore: add trace.Compiler.step 2022-08-11 18:40:13 -07:00
Leonardo de Moura
5dbb907b56 feat: new toLCNF 2022-08-11 18:40:13 -07:00
Leonardo de Moura
3d79581f6b feat: basic LCNF conversion 2022-08-11 18:40:13 -07:00
pcpthm
cbe9adbe9e fix: ac_rfl in subgoal 
Closes #1202
 2022-08-11 07:16:38 -07:00
Gabriel Ebner
067f8e6449 feat: Std.TypeName and Std.Dynamic 2022-08-10 06:31:46 -07:00
Leonardo de Moura
3c6c395e44 feat: add TerminalCases.lean 2022-08-07 22:05:19 -07:00
Leonardo de Moura
7dbfaf9b75 fix: bug at mkSizeOfSpecLemmaInstance 
closes #1441
 2022-08-07 09:24:18 -07:00
Leonardo de Moura
413db56b89 refactor: simplify runTermElabM and liftTermElabM 2022-08-07 07:35:02 -07:00
Leonardo de Moura
ee70805c35 feat: add LCNF missing cases 2022-08-06 20:23:29 -07:00
Leonardo de Moura
4167b2466a fix: improve heuristic for issue #1419 
The fix #1419 generated two regressions on Mathlib.

Fixes #1435
Fixes #1436
 2022-08-06 09:00:16 -07:00
Leonardo de Moura
bf59ad0efc feat: add new compiler entry point function 2022-08-06 08:05:07 -07:00
Leonardo de Moura
9a16d4afce feat: add CompilerM.lean and LCNF.lean 2022-08-05 21:14:39 -07:00
Leonardo de Moura
deafc315c7 fix: make forall_congr more robust at conv intro 
closes #1426
 2022-08-05 12:38:49 -07:00
Leonardo de Moura
50cecdbb62 chore: add Inhabited MProd and Inhabited PProd instances 
closes #1420
 2022-08-05 11:21:27 -07:00
Leonardo de Moura
55bb8e905a chore: binderIdent normalization 
fixes #1411
 2022-08-04 21:10:02 -07:00
Leonardo de Moura
f0272d9309 feat: multiple namespaces in mutual declarations 2022-08-04 19:18:49 -07:00
Leonardo de Moura
0717bdb66d fix: fixes #1419 2022-08-04 15:44:38 -07:00
Leonardo de Moura
8615c42a5d tests: projection defeq strategy 2022-08-04 15:28:22 -07:00
Leonardo de Moura
84ff8d4a04 feat: store pending contraints during dependent pattern matching 
It is a better solution for issues #1361 and #1279, and it was on the
to-do list for a while.
 2022-08-03 17:45:55 -07:00
Leonardo de Moura
a9e7290e4b refactor: use isDefEq instead of custom unify procedure 
See comment with new issue at #1361
 2022-08-02 18:00:00 -07:00
Leonardo de Moura
fbef8a32e1 feat: add support for stuck class projection function applications at getStuckMVar? 
closes #1408
 2022-08-02 16:01:06 -07:00
Leonardo de Moura
b2f34bdedd feat: improve congr conv tactic 
It has better support for proof irrelevant and `[Decidable p]` arguments
 2022-08-02 04:26:34 -07:00
Leonardo de Moura
076d40f51c feat: use implies_congr at congr tactic, and cleanup 2022-08-02 02:24:50 -07:00
Leonardo de Moura
99413a18ff feat: add congr tactic 2022-08-01 18:44:07 -07:00
Mario Carneiro
5f39370d94 chore: rename skip conv to rfl and add no-op skip 2022-08-01 13:54:36 -07:00
Mario Carneiro
df85fee62c chore: rename ac_refl to ac_rfl 2022-08-01 06:53:08 -07:00
Leonardo de Moura
37af11ae20 fix: unused match-syntax alternatives are silently ignored 
closes #1371
 2022-07-31 06:00:08 -07:00
Leonardo de Moura
3dfa895bf0 feat: OfNat instance postprocessor 
Closes #1389
 2022-07-30 08:35:45 -07:00
Leonardo de Moura
012cb13f51 feat: add [elabAsElim] elaboration strategy 2022-07-28 20:08:29 -07:00
Leonardo de Moura
a6c53cf974 fix: fixes #1380 2022-07-28 15:14:50 -07:00
Sebastian Ullrich
a2ccf8f122 feat: accept keywords as constructor names 2022-07-28 12:46:28 -07:00
Leonardo de Moura
ee6e2036dd feat: allow relations in Type at Trans 
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Calc.20mode/near/291214574
 2022-07-28 10:13:01 -07:00
Leonardo de Moura
d267b38a91 fix: disable "error to sorry" and "error recovery" at failIfSuccess 
closes #1375
 2022-07-27 17:09:34 -07:00
Leonardo de Moura
49ce4408df feat: validate parametric local instances 
Closes #1373
 2022-07-27 16:09:56 -07:00
Leonardo de Moura
ed7f502e54 feat: doc string support for register_simp_attr, register_option, register_builtin_option, declare_config_elab 
see #1374
 2022-07-26 18:46:23 -07:00
Leonardo de Moura
43c787d1c6 feat: synthesize implicit structure fields in the structure instance notation 
closes #1305
 2022-07-26 13:24:57 -07:00
Leonardo de Moura
e68e448070 fix: convert inductive type instance implicit parameters to implicit when building SizeOf instance 
It is better for TC resolution since the parameter can be inferred by
typing constraints, and it addresses issue #1373
 2022-07-26 12:42:47 -07:00
Leonardo de Moura
385cfa6001 fix: fixes #1372 2022-07-26 05:51:02 -07:00
Leonardo de Moura
db7e546155 fix: Match.unify? 
closes #1361
 2022-07-25 20:30:01 -07:00
Leonardo de Moura
b3b2a07ed0 feat: support dotted notation and named arguments in patterns 2022-07-25 18:19:32 -07:00