max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
27099 commits 1 branch 0 tags 5.3 GiB
Commit graph

384 commits

Author SHA1 Message Date
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
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