Leonardo de Moura
|
1c1e6d79a7
|
feat: add equality proof for named patterns
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.
closes #501
|
2022-01-18 12:43:01 -08:00 |
|
Leonardo de Moura
|
cd903bde77
|
refactor: [s : Setoid α] => {s : Setoid α} or (s : Setoid α)
See comment at https://github.com/leanprover/lean4/issues/952#issuecomment-1015265136
cc @gebner
|
2022-01-18 09:24:06 -08:00 |
|
Leonardo de Moura
|
bac91b9b5b
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Leonardo de Moura
|
83b69bc340
|
refactor: move Classical.choice and Nonempty to Prelude
|
2022-01-14 15:59:11 -08:00 |
|
Leonardo de Moura
|
e15a656fd2
|
fix: remove @[reducible] annotation from Function.comp and Function.const
closes #813
|
2021-11-23 07:29:25 -08:00 |
|
tydeu
|
3f867acfd7
|
feat: decidable Prop Eq based on propext
|
2021-11-05 14:09:53 -07:00 |
|
Leonardo de Moura
|
094b70c3d4
|
feat: add notation for Sum and PSum
|
2021-09-25 18:24:27 -07:00 |
|
Leonardo de Moura
|
0a898965a3
|
chore: use snake_case for user-facing tactic names
|
2021-09-16 10:23:12 -07:00 |
|
Leonardo de Moura
|
6fb2a2b47b
|
chore: remove ≅ notation for HEq
We don't really needed it here.
|
2021-09-15 08:06:32 -07:00 |
|
Leonardo de Moura
|
ab63382158
|
feat: add helper functions for optimized noConfusion
|
2021-09-06 10:33:34 -07:00 |
|
Leonardo de Moura
|
33a0da8c6f
|
chore: remove simp annotation from PUnit.eq_punit
closes #635
|
2021-08-19 11:22:13 -07:00 |
|
Leonardo de Moura
|
8d90872d28
|
chore: add not_not_intro
|
2021-08-17 21:32:32 -07:00 |
|
François G. Dorais
|
358a129d78
|
fix: protect rfl
|
2021-08-07 13:25:54 -07:00 |
|
Leonardo de Moura
|
9cc94296e5
|
chore: remove staging workaround theorems
|
2021-08-07 12:52:31 -07:00 |
|
Leonardo de Moura
|
a821dcbff2
|
chore: enforce naming convention for theorems
see issue #402
fix: `ElabTerm.lean`
|
2021-08-07 12:48:38 -07:00 |
|
Leonardo de Moura
|
ea37a29e4c
|
chore: remove TODO
|
2021-08-02 20:25:29 -07:00 |
|
Leonardo de Moura
|
cfb7e27b87
|
fix: isStructure vs isStructureLike
|
2021-08-02 18:54:19 -07:00 |
|
François G. Dorais
|
1db0bca914
|
fix: protect Equiv
|
2021-07-02 10:17:38 -07:00 |
|
Leonardo de Moura
|
f4a7ffd8c8
|
chore: fix codebase and tests
|
2021-06-29 17:14:52 -07:00 |
|
Sebastian Ullrich
|
6857076df4
|
feat: leanpkg build without external dependencies
|
2021-05-30 17:29:54 +02:00 |
|
Sebastian Ullrich
|
a02c6fd3eb
|
chore: adapt stdlib & tests
|
2021-05-20 15:17:36 -07:00 |
|
Leonardo de Moura
|
4dabfef0e3
|
chore: remove done
|
2021-05-15 18:57:27 -07:00 |
|
Leonardo de Moura
|
c7096f54a2
|
feat: injectivity theorems for types defined in the prelude
|
2021-05-14 18:32:26 -07:00 |
|
Leonardo de Moura
|
f850820029
|
feat: add mkInjectiveTheorems
|
2021-05-13 22:09:50 -07:00 |
|
Sebastian Ullrich
|
99864bbb31
|
chore: reintroduce ∅ as regular notation
|
2021-05-06 22:41:23 +02:00 |
|
Leonardo de Moura
|
9552b6c95f
|
feat: add Macro.hasDecls and Macro.getCurrNamespace
We need update stage0, and cleanup
|
2021-04-23 17:51:28 -07:00 |
|
Sebastian Ullrich
|
8895ed47e5
|
refactor: clean up Thunk
Fixes a bug in the native implementation of `Thunk.bind` by deleting it
|
2021-04-22 20:29:08 -07:00 |
|
Leonardo de Moura
|
3a80e87793
|
chore: #405 step 1
|
2021-04-22 20:03:48 -07:00 |
|
Leonardo de Moura
|
b3ec00b00a
|
chore: use "discriminant refinement"
|
2021-03-24 10:43:43 -07:00 |
|
Leonardo de Moura
|
d03f5fe318
|
feat: add trivial extensible (macro) tactic
|
2021-03-24 09:50:56 -07:00 |
|
Leonardo de Moura
|
2dfd262e4d
|
chore: cleanup
|
2021-03-24 09:50:56 -07:00 |
|
Leonardo de Moura
|
c54a7c8ccc
|
chore: make HasEquiv more general
|
2021-03-13 07:02:35 -08:00 |
|
Leonardo de Moura
|
e5f1bd2eb9
|
chore: fix Core.lean
|
2021-03-07 12:08:37 -08:00 |
|
Leonardo de Moura
|
e841f16738
|
fix: typo in theorem
`()` is `Unit`
|
2021-03-03 19:50:11 -08:00 |
|
Leonardo de Moura
|
162062b3de
|
feat: improve Lawful.lean
|
2021-02-23 12:38:00 -08:00 |
|
Leonardo de Moura
|
d0574d8eb1
|
feat: add LawfulMonad for StateT
|
2021-02-21 10:52:53 -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
|
99ba21a881
|
chore: annotations for simp
|
2021-02-15 17:04:47 -08:00 |
|
Leonardo de Moura
|
aae8a35150
|
feat: add ForIn type class
|
2021-02-04 17:59:44 -08:00 |
|
Leonardo de Moura
|
4a19a5d2a4
|
refactor: move Eq.trans to Prelude.lean
We need it at `SizeOf.lean`
|
2021-01-27 18:27:04 -08:00 |
|
Leonardo de Moura
|
be7ddef689
|
refactor: move congr and congrFun to Prelude.lean
We use them to generate the `sizeOf` lemmas.
|
2021-01-25 17:18:08 -08:00 |
|
Sebastian Ullrich
|
0c91b3769e
|
chore: replace variables in src/
|
2021-01-22 14:36:05 +01:00 |
|
Leonardo de Moura
|
ad913de340
|
refactor: define SizeOf before Core.lean
|
2021-01-20 17:07:02 -08:00 |
|
Leonardo de Moura
|
244b72befd
|
feat: simpArrow
|
2021-01-01 17:15:15 -08:00 |
|
Leonardo de Moura
|
ce09e795b9
|
feat: finalizeProof at rewrite step
|
2021-01-01 11:33:34 -08:00 |
|
Leonardo de Moura
|
4a06057410
|
feat: simp
|
2020-12-31 15:44:18 -08:00 |
|
Leonardo de Moura
|
3b6d65c3c3
|
chore: use deriving Inhabited
|
2020-12-13 10:09:20 -08:00 |
|
Leonardo de Moura
|
d734a2605b
|
chore: adjust stdlib
|
2020-11-29 17:01:56 -08:00 |
|
Leonardo de Moura
|
e21b4a6399
|
feat: nicer syntax for unification hints
|
2020-11-27 19:18:18 -08:00 |
|
Leonardo de Moura
|
ebba9d119d
|
feat: unification hints
|
2020-11-27 18:12:49 -08:00 |
|