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
Leonardo de Moura
f08b542068
chore: add Nat.add_mul and Nat.mul_add for tutorial
2021-08-25 06:44:12 -07:00
Wojciech Nawrocki
e3d866bc03
feat: initial TraceExplorer
...
Motivation: trace messages from systems such as instance synthesis or defeq checks can be massive and it is hard to find the relevant info within. We provide an interactive TraceExplorer component to do this.
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
7babcc2425
fix: tail-recursion in Format pretty-printer
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
bc8027cdc6
perf: speed up String.intercalate
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
528283bc7d
feat: MonadPrettyFormat
2021-08-24 08:57:41 -07:00
Leonardo de Moura
4dccaa963b
feat: add List.mapTR and csimp lemma
2021-08-22 09:32:19 -07:00
Leonardo de Moura
ec6af1ba26
feat: use simple List.append definition and add csimp theorem
2021-08-21 16:11:54 -07:00
Leonardo de Moura
3b240d9a14
feat: use simple List.length definition and add csimp theorem
2021-08-21 13:11:06 -07:00
