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
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
d6f778bec4
refactor: arbitrary without explicit arguments
...
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
2020-11-25 09:07:38 -08:00
Leonardo de Moura
f456e006dc
chore: test instance ... where
2020-11-23 18:24:23 -08:00
Leonardo de Moura
304c80d610
feat: use <|
2020-11-19 09:03:38 -08:00
