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
Leonardo de Moura
7066619123
refactor: define Nat.le using inductive type
2021-08-20 19:39:45 -07:00
Leonardo de Moura
a15a36b8d3
chore: cleanup Subarray instances
2021-08-13 19:29:09 -07:00
Leonardo de Moura
24fe2875c6
chore: change Pow class
...
Based on the suggestion at https://github.com/leanprover/lean4/issues/433
2021-08-12 13:59:55 -07:00
Leonardo de Moura
9cc94296e5
chore: remove staging workaround theorems
2021-08-07 12:52:31 -07:00
Leonardo de Moura
a821dcbff2
chore: enforce naming convention for theorems
...
see issue #402
fix: `ElabTerm.lean`
2021-08-07 12:48:38 -07:00
Leonardo de Moura
a230fe2d06
fix: forallMetaTelescope issue
...
This commit incorporates the fix at PR #612 , and clean up
`Meta/Basic.lean` using Lean 4 features.
2021-08-06 09:47:10 -07:00
Wojciech Nawrocki
f1b4d9a193
chore: restore non-generic Format
...
Motivation: it is unclear whether this is the best solution for embedding objects in pretty-printer outputs.
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
b022a7c1d2
style: indent
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
9b8e44618d
chore: default to Format Nat
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
a937fa26ba
chore: fewer explicit types
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
f51b80060d
feat: generic tagged Format
2021-08-01 09:58:44 +02:00
Leonardo de Moura
af5ff9ceb2
refactor: move List.takeWhile to Init.Data.List.Basic
...
Motivation: make sure it will be aligned by BinPort
2021-07-31 15:03:33 -07:00
Leonardo de Moura
f10c27dfb7
perf: add workaround for perf issue
...
See issue #361
2021-07-29 08:29:09 -07:00
Wojciech Nawrocki
776a0c71aa
feat: add UInt64 unpackings
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
80d90038ad
feat: add Format tags
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
caa8f7f7b2
chore: expose Substring.prev/next
2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
7aca461a35
fix: hovers on elabFieldName fields
2021-07-19 09:55:37 +02:00
Wojciech Nawrocki
b2d712a766
fix: Substring.splitOn
2021-07-19 09:55:37 +02:00
