Leonardo de Moura
05be43455a
feat: add src/Init/Data/Nat/Linear.lean
2022-02-24 13:45:17 -08:00
Leonardo de Moura
43c2169f78
fix: when performing contextual simplification, and arrow may become a dependent arrow
...
fixes #1024
2022-02-23 18:43:32 -08:00
Leonardo de Moura
0125db40a2
fix: remove [..] annotation from if simp theorems
...
fixes #1025
2022-02-23 16:28:12 -08:00
Leonardo de Moura
902e60c480
feat: add Format.isEmpty
2022-02-23 13:34:25 -08:00
Leonardo de Moura
24249fecd3
feat: helper simp theorems
2022-02-22 16:03:36 -08:00
Leonardo de Moura
8d6750469e
chore: helper Nat theorems
2022-02-22 14:26:50 -08:00
Leonardo de Moura
7f3a3138d0
feat: helper Nat theorems
2022-02-21 08:49:50 -08:00
Leonardo de Moura
ba16903205
feat: add helper theorems
2022-02-19 21:25:44 -08:00
Leonardo de Moura
193859c72c
feat: add helper theorems
2022-02-19 17:53:54 -08:00
Leonardo de Moura
19bcb5fb31
feat: add Array.popWhile and Array.takeWhile
2022-02-19 07:04:52 -08:00
Leonardo de Moura
86328bcb9f
feat: tail recursive List.iota and [csimp] theorem
2022-02-16 11:25:46 -08:00
Leonardo de Moura
bd89bdde8a
fix: core library
...
see #1018
2022-02-15 12:12:56 -08:00
Sebastian Ullrich
54522006f4
refactor: List.get: take Fin to align with Array.get
...
/cc @leodemoura
2022-02-15 18:41:22 +01:00
Leonardo de Moura
ee9fcd30e8
fix: mark Nat.decEq as [reducible]
...
It is used by the `noConfusionType` construction for enumeration types,
and we want it to reduce even when the reducibility setting is
`TransparencyMode.reducible` as for other inductive types.
see issue #1016
2022-02-14 12:00:29 -08:00
Leonardo de Moura
420d0f2a3f
fix: make sure noConfusionTypeEnum and noConfusionEnum fully reduce even reducibility setting is set to TransparencyMode.reducible
...
The previous definition would not fully reduce since `ite` and `dite`
are not tagged as `[reducible]`.
see issue #1016
2022-02-14 11:39:18 -08:00
Leonardo de Moura
9cfa728eac
chore: remove workaround for issue #1013
2022-02-11 09:32:29 -08:00
Leonardo de Moura
77bbaf82df
feat: decidable equality for arrays
2022-02-10 17:31:03 -08:00
Leonardo de Moura
712d6726e4
feat: rename tactic byCases => by_cases
2022-02-10 17:11:07 -08:00
Leonardo de Moura
1491253479
feat: helper simp theorems
2022-02-10 17:06:16 -08:00
Leonardo de Moura
1d5da63482
chore: simplify Array.isEqvAux
2022-02-10 16:51:47 -08:00
Leonardo de Moura
6b6c44c559
feat: add helper lemma
2022-02-10 16:51:32 -08:00
Sebastian Ullrich
2c7d67d498
fix: make info of fields synthesized by structure update synthetic
2022-02-06 08:50:07 -08:00
Joscha
841d51a7e6
fix: walkDir
2022-02-05 19:55:09 +01:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Gabriel Ebner
55be278cd7
fix: ensure motive of matches is Bool
2022-02-03 18:17:27 +01:00
larsk21
ce92672c3a
fix: remove explicit Ord Range
2022-02-02 13:03:21 +01:00
larsk21
6cee7a6a31
fix: dedup references in findModuleRefs
2022-02-02 13:03:21 +01:00
Sebastian Ullrich
ce58ded16f
fix: syntax match of literals
...
Fixes #801
2022-01-29 08:40:03 -08:00
Leonardo de Moura
d4f7899591
chore: avoid code duplication setting Simp.Config
2022-01-24 18:57:31 -08:00
Leonardo de Moura
a9659afa50
chore: remove old decls
2022-01-20 15:35:19 -08:00
Leonardo de Moura
6f416147b4
chore: rename coeM and liftCoeM
2022-01-20 15:33:17 -08:00
Leonardo de Moura
2192e6148b
chore: remove coe, coeSort, and coeFun abbreviations
...
The notation `↑ e` is now expanded eagerly.
See #403
2022-01-20 15:19:06 -08:00
Leonardo de Moura
3c17755730
chore: prepare to remove coe definitions
...
The notation `↑ e` will eagerly expand the coersion.
See #403
2022-01-20 15:07:54 -08:00
Leonardo de Moura
f9fa24435d
chore: remove problematic instance hasOfNatOfCoe
...
See #403
See https://github.com/leanprover-community/mathport/issues/94
2022-01-20 14:47:25 -08:00
tydeu
8e79d88d29
feat: liftOption
2022-01-19 12:22:05 +01:00
Leonardo de Moura
a21265281b
chore: remove temporary workaround
2022-01-18 14:11:54 -08:00
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
874aadd7e3
chore: update namedPattern signature
...
Remark: It is not being used yet.
2022-01-17 17:21:18 -08:00
Leonardo de Moura
0f217eb4c1
chore: prepare to change namedPattern signature
2022-01-17 17:13:09 -08:00
Leonardo de Moura
2c690926cf
feat: update namedPattern parser
2022-01-17 16:49:20 -08:00
Leonardo de Moura
de11f7e1bc
feat: add sizeOf spec lemmas as simp theorems
2022-01-17 16:14:38 -08:00
Gabriel Ebner
561a869e49
fix: provide reference implementation for Array.modify
2022-01-17 12:41:12 -08:00
Leonardo de Moura
bac91b9b5b
chore: remove arbitrary
2022-01-15 12:14:27 -08:00
Leonardo de Moura
a3a134a297
chore: export Inhabited.default
2022-01-15 11:50:28 -08:00
Leonardo de Moura
b0d9c16c7a
chore: rename PointedType => NonemptyType
2022-01-15 11:43:53 -08:00
Leonardo de Moura
e3241e82bc
feat: define PointedType as { α : Type u // Nonempty α }
2022-01-14 20:36:51 -08:00
Leonardo de Moura
acd482c5f2
feat: define Array.modify without using Inhabited
2022-01-14 19:47:42 -08:00
Leonardo de Moura
c34adb7dd5
feat: allow partial definitions to be define if type is non empty
2022-01-14 16:50:36 -08:00
Leonardo de Moura
f1adedb2de
feat: add Classical.ofNonempty
2022-01-14 15:59:11 -08:00
