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
Leonardo de Moura
284177a80a
feat: missing instances and getOp for byte/float arrays
2021-10-18 16:54:56 -07:00
Leonardo de Moura
2fd024c26f
feat: add support for foldlM, foldl, ForIn instances for byte/float arrays
2021-10-18 16:54:56 -07:00
Leonardo de Moura
d03aaec944
feat: expose new float/byte array primitives
2021-10-18 16:54:56 -07:00
Siddharth
da4ad465d0
feat: un-inline float intrinsics into runtime. ( #694 )
...
* outline all intrinsics into the runtime.
This is necessary to support backends such as LLVM which do not emit C.
* fix style
2021-10-18 07:20:04 -07:00
Leonardo de Moura
f64753c106
test: simplify ac_expr.lean
...
We don't want to avoid proofs at `List.getIdx` and `Expr` when doing proofs by reflection.
The new encoding avoids that by using the fact that `vars` in
`Context` should never be empty.
To be honest, the best approach is still the old `unit`. We can just
rename it to `inhabitant` to make sure users don't assume it is the
unit of the AC operator. Then, we can just set it with the first element
of `vars` and avoid proofs at `denote`.
2021-10-06 17:56:26 -07:00
Leonardo de Moura
9d0fe5cbf9
chore: add simp rule Nat.lt x y = (x < y)
2021-10-06 16:37:58 -07:00
Leonardo de Moura
d4509878bb
feat: add WellFoundedRelation for termination_by
2021-09-25 17:21:03 -07:00
Leonardo de Moura
4a8679a57c
feat: add Subarray.popFront
2021-09-25 08:35:41 -07:00
Leonardo de Moura
bb98057098
refactor: avoid wf suffix
2021-09-21 12:57:08 -07:00
Leonardo de Moura
9032ddd773
chore: add simp lemma for converting Nat.add back into + notation
2021-09-08 14:58:13 -07:00
Leonardo de Moura
3714cf16ec
refactor: lazy evaluation for <|>
...
see #617
2021-09-07 17:06:10 -07:00
Leonardo de Moura
e4410cfbf8
chore: missing Fin instances
2021-09-05 16:09:18 -07:00
Leonardo de Moura
9bb5d4dc93
chore: Nat.ltWf => Nat.lt_wf
2021-09-02 07:51:41 -07:00
Leonardo de Moura
2a6473641a
chore: fix theorem name
2021-08-30 10:10:54 -07:00
Leonardo de Moura
b205cfaaf2
chore: missing annotations at List.mapTR
2021-08-27 10:17:49 -07:00
Leonardo de Moura
8ba10521e6
feat: add theorem for tutorial
2021-08-26 12:58:02 -07:00
Leonardo de Moura
00193fb953
feat: add theorems for tutorial
2021-08-26 12:13:15 -07:00
Leonardo de Moura
795ccf6e2b
chore: add Trans instances for tutorial
2021-08-25 08:50:51 -07:00
