Leonardo de Moura
|
b5f28239af
|
feat: add List helper theorems
|
2022-02-28 15:16:13 -08:00 |
|
Leonardo de Moura
|
89f88b1caa
|
feat: simplify nested arith expressions
|
2022-02-27 09:01:52 -08:00 |
|
Leonardo de Moura
|
812cc72285
|
chore: add helper theorems
|
2022-02-25 17:04:04 -08:00 |
|
Leonardo de Moura
|
3f636b9f83
|
feat: add Lean.Meta.Linear.Nat.simpCnstr?
|
2022-02-25 16:27:21 -08:00 |
|
Leonardo de Moura
|
346930af9d
|
feat: add ExprCnstr.eq_of_toNormPoly_eq
|
2022-02-25 14:55:20 -08:00 |
|
Leonardo de Moura
|
b8bed6fb5c
|
feat: add LawfulBEq class
|
2022-02-25 13:35:08 -08:00 |
|
Leonardo de Moura
|
3b130ee42f
|
feat: add Poly.toExpr
|
2022-02-25 12:31:30 -08:00 |
|
Leonardo de Moura
|
be2e2cb70e
|
chore: adjust proofs affected by update stage0
|
2022-02-24 17:20:17 -08:00 |
|
Leonardo de Moura
|
05be43455a
|
feat: add src/Init/Data/Nat/Linear.lean
|
2022-02-24 13:45:17 -08:00 |
|
Leonardo de Moura
|
902e60c480
|
feat: add Format.isEmpty
|
2022-02-23 13:34:25 -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
|
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
|
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 |
|
Leonardo de Moura
|
12e2a79170
|
chore: fix codebase after removing auto pure
|
2022-02-03 18:08:14 -08: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 |
|
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 |
|
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
|
acd482c5f2
|
feat: define Array.modify without using Inhabited
|
2022-01-14 19:47:42 -08:00 |
|
Leonardo de Moura
|
7fe6881c42
|
feat: use new termination_by syntax
|
2022-01-12 16:23:25 -08:00 |
|
Leonardo de Moura
|
381f66428a
|
chore: use termination_by'
We are going to define a higher level syntax for `termination_by`.
|
2022-01-11 15:00:53 -08:00 |
|
Leonardo de Moura
|
93f3773d83
|
chore: cleanup
|
2022-01-10 16:25:07 -08:00 |
|
Leonardo de Moura
|
dae3489fe2
|
feat: remove partials from Init/Data/Array/Basic.lean
|
2022-01-10 16:05:33 -08:00 |
|
Leonardo de Moura
|
0dd3ce0598
|
chore: fix test
|
2022-01-10 14:31:23 -08:00 |
|
Leonardo de Moura
|
16b4aa81e5
|
chore: add helper lemmas for well-founded recursion
|
2022-01-10 14:07:35 -08:00 |
|
Leonardo de Moura
|
241db0fed6
|
chore: fix name
|
2022-01-10 13:20:49 -08:00 |
|
Sebastian Ullrich
|
bbfcb1cfb2
|
perf: allocation-free for i in [n:m] do
|
2022-01-03 07:03:56 -08:00 |
|
Mario Carneiro
|
f22f699d62
|
feat: split replicate / replicateTR with @[csimp]
|
2021-12-18 10:58:57 -08:00 |
|
Mario Carneiro
|
51a78fd7af
|
fix: change argument order of List.get[!?D]
|
2021-12-17 14:21:00 -08:00 |
|
Joe Hendrix
|
5a307a93ac
|
fix: bug at ByteArray.copySlice
|
2021-12-16 11:05:19 +01:00 |
|
Gabriel Ebner
|
45bcef5dab
|
refactor: server: use String.firstDiffPos to find changes
This is necessary so that we do not reprocess the whole file if
incremental sync is disabled.
|
2021-12-14 11:55:34 -08:00 |
|
Leonardo de Moura
|
68bd55af32
|
chore: fix codebase
|
2021-12-10 13:12:09 -08:00 |
|
Leonardo de Moura
|
84f374702d
|
feat: add fields isInstance and isType to InteractiveHypothesis
see https://github.com/leanprover/vscode-lean4/issues/76
|
2021-12-10 09:08:55 -08:00 |
|
Sebastian Ullrich
|
978e94272c
|
feat: String.replace
|
2021-11-18 09:42:35 +01:00 |
|
Leonardo de Moura
|
352391bfcb
|
chore: remove mpz_get_d dependency
|
2021-10-26 12:40:20 -07:00 |
|
Gabriel Ebner
|
95b769cd5d
|
fix: add missing borrow annotations
|
2021-10-26 11:51:30 -07:00 |
|
Gabriel Ebner
|
61e0eab23f
|
refactor: reimplement ofScientific for floats
|
2021-10-26 11:51:30 -07:00 |
|
Gabriel Ebner
|
bfc74decde
|
feat: add info field to Syntax.node
|
2021-10-26 20:19:27 +02:00 |
|
Leonardo de Moura
|
4e70a20292
|
feat: add more Nat "re-packing" simp theorems
|
2021-10-19 06:43:07 -07:00 |
|
Leonardo de Moura
|
c425397b45
|
feat: Hashable instances for UInt8 and UInt16
|
2021-10-18 17:19:39 -07:00 |
|