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

2057 commits

Author SHA1 Message Date
Leonardo de Moura
e15a656fd2 fix: remove @[reducible] annotation from Function.comp and Function.const 
closes #813
 2021-11-23 07:29:25 -08:00
Leonardo de Moura
9fde1d53b7 chore: adjust proofs affected by struct eta 
closes #777
 2021-11-23 06:23:50 -08:00
Sebastian Ullrich
978e94272c feat: String.replace 2021-11-18 09:42:35 +01:00
Sebastian Ullrich
d8d7eba6c5 feat: liftExcept 2021-11-09 16:58:13 +01:00
Leonardo de Moura
743810b77a feat: use binrel_no_prop% to define == notation 
fixes #764
 2021-11-09 07:46:10 -08:00
tydeu
7fcfb78fd5 feat: use BaseIO at MonadLift (ST IO.RealWorld) 2021-11-09 09:11:33 +01:00
Leonardo de Moura
7e0bc23e5d chore: cleanup syntax 2021-11-05 15:03:57 -07:00
tydeu
3f867acfd7 feat: decidable Prop Eq based on propext 2021-11-05 14:09:53 -07:00
Mac
eb5852448e
feat: generalize IO task functions to BaseIO := EIO Empty (#744) 
* feat: generalize `asTask`/`bindTask`/`mapTask` to `EIO`

* feat: generalize task functions to the `EIO Empty` monad

* chore: fix test + correct doc

* feat: further generalize task functions to `RealM := EIO Empty`

* chore: `RealM`/Task API touch-ups

* refactor: `abbrev RealM` -> `def BaseIO`

* chore: remame args / remove `EIO.toBaseIO_` as per code review

* refactor: use `BaseIO` at `checkCanceled`/`getNumHeartbeats`

* chore: fix `lean_io_bind_task_fn` signature error
 2021-11-04 15:37:55 -07:00
Sebastian Ullrich
b5e7b2ab6e feat: Lean.githash 2021-11-04 15:29:48 -07: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
fbdb68b669 feat: conv in conv 
Featured suggested at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/257193307
 2021-10-22 13:53:56 -07: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
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