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
Leonardo de Moura
ab3861ff62
chore: remove unnecessary "c"
...
and avoid compilation warning messages.
2021-10-18 07:34:17 -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
Gabriel Ebner
34eda689a1
fix: use eraseMacroScopes on trace classes
2021-10-08 11:13:19 -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
7f660af4c6
feat: add repeat tactic to conv mode
2021-10-06 14:05:44 -07:00
Leonardo de Moura
c908eec8e5
chore: remove temp priority := high
2021-10-02 17:31:55 -07:00
Leonardo de Moura
c24cd877c8
chore: define if-then-else again as a macro
...
We can do it using the new auxiliary notation `let_mvar%` and
`wait_if_type_mvar%`.
2021-10-02 17:30:06 -07:00
Leonardo de Moura
acd21052c0
chore: remove old notation
2021-10-02 15:06:40 -07:00
Leonardo de Moura
b7281e9fe2
fix: instruct pretty printer to add a line break after each calc step
...
It should fix https://github.com/leanprover/mathport/issues/26
2021-10-02 11:38:10 -07:00
Leonardo de Moura
88c73f1daa
chore: remove old if-then-else parser and elaborator
2021-09-30 20:33:58 -07:00
Leonardo de Moura
7ea23a0f37
chore: reduce priority of old if-then-else parser
2021-09-30 20:31:54 -07:00
Leonardo de Moura
a5502e652c
chore: activate builtin if-then-else elaborator
2021-09-30 20:29:49 -07:00
Leonardo de Moura
b85d95b7b6
fix: panic in monadic polymorphic code
...
fixes #695
2021-09-28 17:46:19 -07:00
Leonardo de Moura
4c051896df
refactor: sizeofMeasure => sizeOfWFRel
...
This commit also makes the first argument of `sizeOfWFRel` implicit.
2021-09-27 19:06:10 -07:00
Leonardo de Moura
094b70c3d4
feat: add notation for Sum and PSum
2021-09-25 18:24:27 -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
10a38aef3c
chore: remove class WellFoundedRelation
...
It is dead code.
2021-09-21 12:57:08 -07:00
Leonardo de Moura
f2a418a7ae
chore: smartUnfolding cleanup
...
We remove dead code, update comments, and add new tests
See #445
2021-09-19 15:29:11 -07:00
Leonardo de Moura
35d9589401
feat: add MonadControl m (OptionT m)
2021-09-19 14:20:26 -07:00
Leonardo de Moura
fc1ec438b8
fix: Repr Name instance
2021-09-18 15:29:32 -07:00
Leonardo de Moura
2a9ba9f795
fix: add support for hierachical names containing numerical parts
...
closes #677
2021-09-17 19:21:49 -07:00
Leonardo de Moura
a823ebdbe0
chore: make it clear how it is being parsed
...
We are planning to change the `<|>` precedence here.
2021-09-16 13:41:01 -07:00
Leonardo de Moura
0a898965a3
chore: use snake_case for user-facing tactic names
2021-09-16 10:23:12 -07:00
Leonardo de Moura
c2a5e37c60
feat: simp discharger
2021-09-16 10:11:27 -07:00
Sebastian Ullrich
08c2c31fcd
feat: IO.FS.removeDir(All)
2021-09-16 07:01:37 -07:00
Daniel Selsam
8d370f151f
fix: space before 'at' in location
2021-09-15 18:41:26 +02:00
Leonardo de Moura
6fb2a2b47b
chore: remove ≅ notation for HEq
...
We don't really needed it here.
2021-09-15 08:06:32 -07:00
Leonardo de Moura
d2240a99e5
feat: add erw tactic back as a macro
2021-09-12 19:29:12 -07:00
Leonardo de Moura
42436254ee
fix: code
2021-09-12 19:11:21 -07:00
Leonardo de Moura
bfa1c86b24
feat: add optional config parser to rewrite tactics
2021-09-12 19:05:15 -07:00
Leonardo de Moura
ea37c64b52
feat: add Meta.Rewrite.Config
2021-09-12 18:44:08 -07:00
Leonardo de Moura
71229f45fb
chore: "upgrate" to doc string
2021-09-12 18:30:08 -07:00
Leonardo de Moura
8c82302aca
refactor: add config syntax and macro for boilerplate code
2021-09-12 18:09:19 -07:00
Leonardo de Moura
218b9c87b0
feat: expose APIs for creating IO.Error objects
2021-09-11 17:14:43 -07:00
Leonardo de Moura
4630c9af7c
feat: add congruence lemmas for let-expressions
2021-09-10 18:53:23 -07:00
Leonardo de Moura
1576040c87
chore: remove workaround
2021-09-09 19:30:31 -07:00
Leonardo de Moura
f5a4b30d5f
fix: broken proof
2021-09-09 18:11:05 -07:00
Leonardo de Moura
5154f462f8
feat: add reduce conv tactic
2021-09-09 17:47:10 -07:00
Leonardo de Moura
496cc92ae9
feat: add simpMatch helper conv tactic
2021-09-09 17:29:32 -07:00
Leonardo de Moura
b5b5370181
feat: add delta to conv mode
2021-09-09 13:07:33 -07:00
Leonardo de Moura
4087525cba
feat: add delta tactic
2021-09-09 13:07:33 -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
716ffecf89
chore: add sorry tactic
2021-09-08 08:10:37 -07:00
