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

4180 commits

Author SHA1 Message Date
Gabriel Ebner
430d7d05d6 feat: add derive handler for Nonempty 2022-12-22 03:48:15 +01:00
Gabriel Ebner
572ffe77e3 fix: implement assertAfter using revert 2022-12-21 21:42:07 +01:00
Sebastian Ullrich
96ccf192e8 fix: parenthesize by optParam values 2022-12-20 18:10:39 +01:00
Gabriel Ebner
e386d5941e refactor: replace ignoreLevelMVarDepth by levelAssignDepth 2022-12-19 20:14:17 +01:00
Gabriel Ebner
1c8ef51124 fix: make List.toString tail-recursive 2022-12-12 22:58:21 +01:00
Leonardo de Moura
8a573b5d87 fix: fixes #1900 2022-12-02 10:04:01 -08:00
Leonardo de Moura
50fc4a6ad8 fix: fixes #1907 2022-12-02 08:59:16 -08:00
Gabriel Ebner
b0cadbc1fa fix: support escaped field names in deriving FromJson/ToJson 2022-12-02 03:48:19 +01:00
Gabriel Ebner
3d1571896c fix: support escaped field names in dot-notation 2022-12-02 03:48:19 +01:00
Leonardo de Moura
ffb0f42aae fix: fixes #1901 2022-12-01 08:39:06 -08:00
Leonardo de Moura
0dda3a8c02 fix: include instance implicits that depend on outParams at outParamsPos 
This fixes the fix for #1852
 2022-12-01 06:11:48 -08:00
Leonardo de Moura
5a151ca64c chore: fix tests 2022-11-30 17:52:37 -08:00
Leonardo de Moura
3e45060dd5 fix: disable implicit lambdas for local variables without type information 
Problem reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/why.20doesn't.20this.20unify.3F/near/312806870
 2022-11-29 14:33:16 -08:00
Gabriel Ebner
bdbab653fd fix: synthesize tc instances before propagating expected type 2022-11-29 08:16:09 -08:00
Leonardo de Moura
c510d16ef5 fix: fixes #1808 2022-11-28 07:48:54 -08:00
Leonardo de Moura
36cc7c23b6 fix: fixes #1886 2022-11-28 06:50:44 -08:00
Sebastian Ullrich
42a080fae2 fix: comments ending in --/ 
Fixes #1883
 2022-11-25 10:32:49 +01:00
Leonardo de Moura
c53c5b5e16 fix: fixes #1882 
Better support for `intro <type-ascription>`.
It was treating it as a pattern before this commit.
 2022-11-24 12:40:25 -08:00
Leonardo de Moura
9d8b324f8d fix: fixes #1869 
Better support for simplifying class projections.
 2022-11-24 11:56:36 -08:00
Leonardo de Moura
0694731af8 fix: fixes #1870 2022-11-23 05:49:19 -08:00
Leonardo de Moura
51a29098ab fix: fixes #1852 2022-11-19 09:37:52 -08:00
Leonardo de Moura
22e96c71e9 fix: fixes #1850 2022-11-19 09:18:12 -08:00
Leonardo de Moura
a5ab59a413 fix: fixes #1851 2022-11-19 07:01:02 -08:00
Leonardo de Moura
a7107aedb3 fix: fixes #1848 2022-11-18 08:49:10 -08:00
Mario Carneiro
f74fee07e6
doc: document Init.Data.List.Basic (#1828) 
* doc: document Init.Data.List.Basic

* Apply suggestions from code review

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-11-18 06:16:50 -08:00
Leonardo de Moura
d2a5ea137d fix: fixes #1842 2022-11-16 17:29:41 -08:00
Leonardo de Moura
edadd8c034 fix: fixes #1841 
This commit adds the configuration option
`ApplyConfig.approx` (available in Lean 3), and sets it to true by
default like in Lean 3.
 2022-11-16 14:46:05 -08:00
Leonardo de Moura
7b03d9719c fix: fixes #1679 2022-11-16 13:15:53 -08:00
Leonardo de Moura
98922b878a fix: fixes #1815 2022-11-15 17:08:54 -08:00
Leonardo de Moura
8225be2f0e feat: ensure projections are not reducing at DiscrTree V (simpleReduce := true) 
Now, the `simp` discrimination tree does not perform `iota` nor reduce
projections.
 2022-11-15 16:47:12 -08:00
Leonardo de Moura
1b0c2f7157 feat: parameterize DiscrTree indicating whether non trivial reductions are allowed or not when indexing/retrieving terms 2022-11-15 16:47:12 -08:00
Leonardo de Moura
1cc58e60ef fix: fixes #1829 2022-11-15 08:31:36 -08:00
Sebastian Ullrich
591eccee4f chore: move expensive test to beginning of test block 2022-11-14 15:46:34 +01:00
Leonardo de Moura
5654d8465d fix: fixes #1822 2022-11-13 18:13:29 -08:00
Leonardo de Moura
a87f0e25de feat: add compiler.checkTypes for sanity checking 2022-11-13 17:45:21 -08:00
Leonardo de Moura
ca0fb21df4 fix: fixes #1813 
Remark: modifies the value for the `mid` priority.
See new note at `Init/Notation.lean`
 2022-11-10 16:09:21 -08:00
Leonardo de Moura
c147059fd7 fix: fixes #1812 2022-11-10 08:58:09 -08:00
Leonardo de Moura
b4d13a8946 refactor: LetExpr => LetValue 
We use "let value" in many other places in the code base.
 2022-11-07 18:51:07 -08:00
Leonardo de Moura
d11697cbf7 chore: fix some tests 2022-11-07 18:18:06 -08:00
Scott Morrison
d0dc9a2f90
fix: reorder goals after specialize (#1796) 
* fix: reorder goals after specialize

* fix test
 2022-11-03 06:32:55 -07:00
Mario Carneiro
ad1c23f172 fix: bug in replaceLocalDeclDefEq 
fixes #1615
 2022-11-01 19:18:25 -07:00
Leonardo de Moura
5f38a483f2 fix: congr tactic 
`MVarId.congr?` and `MVarId.hcongr?` should return `none` if an
exception is thrown while applying congruence theorem.

`MVarId.hcongr?` should try `eq_of_heq` before trying to apply
`hcongr` theorem.

closes #1787

BTW: Lean 4 `congr` tactic is applying `assumption`. Lean 3 version does not.
 2022-10-28 08:00:04 -07:00
Leonardo de Moura
0b6b754bca feat: improve apply tactic 
It tries to address what the Mathlib community calls the "apply bug".

cc @digama0
 2022-10-26 16:58:43 -07:00
Leonardo de Moura
f3b1eadb55 feat: copy docstring when copying parent fields 
closes #1730
 2022-10-26 15:43:46 -07:00
Leonardo de Moura
83d8e36773 fix: fixes #1780 2022-10-26 07:46:38 -07:00
Leonardo de Moura
5a8f9ace72 fix: open .. hinding .. should activate scoped attributes 2022-10-26 07:39:06 -07:00
Gabriel Ebner
725aa8b39a refactor: instantiateTypeLevelParams in Lean 2022-10-24 12:23:13 -07:00
Gabriel Ebner
fc304d95c0 feat: Min/Max typeclasses 2022-10-21 14:36:38 -07:00
Leonardo de Moura
aeddcbdc6d fix: disable implicit lambdas at intro <pattern> notation 
See issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/intro.20with.20type.20specified/near/305150215
 2022-10-20 09:04:06 -07:00
Mario Carneiro
dd8bbe9367 fix: catch kernel exceptions in Kernel.{isDefEq, whnf} 
fixes #1756
 2022-10-20 05:38:29 -07:00