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

4019 commits

Author SHA1 Message Date
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
Leonardo de Moura
c418e8d2c5 fix: use useExplicit := false when processing instance ... where ... notation fields 
See new test.
 2022-07-25 16:53:13 -07:00
Leonardo de Moura
c2a13da58d fix: ensure let f | ... and let rec f | ... notations behave like the top-level ones with respect to implici lambdas 
closes #1360
 2022-07-25 16:53:13 -07:00
Leonardo de Moura
a62949c49b refactor: add type LevelMVarId (and abbreviation LMarId) 
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.

cc @bollu
 2022-07-24 17:21:45 -07:00
Leonardo de Moura
e0882e098b chore: avoid stackoverflow in debug build 2022-07-24 14:47:51 -07:00
Leonardo de Moura
2c825de6a1 fix: elim_scalar_array_cases 2022-07-24 14:46:46 -07:00
Leonardo de Moura
5e877b115b feat: improve calc tactic 
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.

Closes #1342
 2022-07-24 14:30:15 -07:00
Leonardo de Moura
c46ef56ac7 perf: avoid blowup at deriving Repr 
The fix is not perfect. I just avoided inlining in some builtin `Repr` instances.
The actual problem is at `ElimDeadBranches.lean`.

Closes #1365
 2022-07-24 13:10:04 -07:00
Leonardo de Moura
5253cc6742 fix: compiler support for FloatArray.casesOn and ByteArray.casesOn 
closes #1311
 2022-07-24 12:36:08 -07:00
Leonardo de Moura
7829be9d54 fix: fixes #1333 2022-07-24 12:19:53 -07:00
Leonardo de Moura
2196a3518e perf: improve lazy_delta_reduction_step heuristic 
It addresses a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/performance.20of.20equality.20with.20projections.2Fmutual/near/288083209
 2022-07-24 11:48:45 -07:00
Leonardo de Moura
6cff1f1813 fix: try to postpone by .. if expectedType? = none 
Reason: it may become `some ..` later. See issue #1359

Closes #1359
 2022-07-24 08:03:25 -07:00
Sebastian Ullrich
5160cb7b0f refactor: remove some unnecessary antiquotation kind annotations 2022-07-23 17:09:32 +02:00
Sebastian Ullrich
1f081ee6cb feat: doc comment support for unif_hint 2022-07-22 14:30:49 +02:00
Sebastian Ullrich
5d187b8beb fix: register tokens in parser quotation 2022-07-21 23:49:57 +02:00