Leonardo de Moura
|
5ff62ebf06
|
feat: check user given path
|
2020-02-05 09:42:26 -08:00 |
|
Leonardo de Moura
|
9993eb9b2b
|
fix: increase scope of try
Motivation: avoid "libc++abi.dylib: terminating with uncaught
exception of type lean::exception ..."
|
2020-02-05 09:27:54 -08:00 |
|
Leonardo de Moura
|
660571ab38
|
fix: closes #109
Fixed myself after wasting time wondering whether a segfault was
coming from today.
cc @cipher1024
|
2020-02-05 09:16:33 -08:00 |
|
Leonardo de Moura
|
92d8688880
|
chore: update stage0
|
2020-02-04 17:49:56 -08:00 |
|
Leonardo de Moura
|
eacff1a448
|
feat: implement withPtrEq and withPtrAddr
|
2020-02-04 17:48:11 -08:00 |
|
Leonardo de Moura
|
38e6961003
|
feat: MutQuot by implementedBy
|
2020-02-04 16:51:08 -08:00 |
|
Leonardo de Moura
|
13aec48069
|
chore: update stage0
|
2020-02-04 16:02:00 -08:00 |
|
Leonardo de Moura
|
ac88b46299
|
feat: MutQuot primitives
|
2020-02-04 15:56:20 -08:00 |
|
Leonardo de Moura
|
850b1c90a0
|
feat: mark as irrelevant functions that return types
|
2020-02-04 15:55:21 -08:00 |
|
Leonardo de Moura
|
6f4dd5441e
|
chore: disable test on windows
|
2020-02-04 14:21:38 -08:00 |
|
Leonardo de Moura
|
362185147e
|
chore: remove unncessary annotation
|
2020-02-04 14:21:26 -08:00 |
|
Leonardo de Moura
|
b5eb64da3a
|
fix: add mkFilePath and try to fix Windows build
|
2020-02-04 11:24:33 -08:00 |
|
Leonardo de Moura
|
d02ff42ade
|
chore: update stage0
|
2020-02-04 10:47:02 -08:00 |
|
Leonardo de Moura
|
3a9f6e4133
|
perf: avoid closure allocations and orelse when next token is not "$"
|
2020-02-04 10:45:41 -08:00 |
|
Leonardo de Moura
|
48be9094b9
|
test: add test for parsing Core.lean
|
2020-02-04 10:15:00 -08:00 |
|
Leonardo de Moura
|
d125966c52
|
chore: fix tests
|
2020-02-04 10:14:31 -08:00 |
|
Leonardo de Moura
|
63434fbb7d
|
chore: add parser tests
|
2020-02-04 10:11:50 -08:00 |
|
Leonardo de Moura
|
01cc87b326
|
chore: update stage0
|
2020-02-04 09:52:19 -08:00 |
|
Leonardo de Moura
|
76677049e2
|
chore: fix precedence of leading tokens
|
2020-02-04 09:44:43 -08:00 |
|
Sebastian Ullrich
|
52a0a0937e
|
feat: check precedence of leading parsers as well
|
2020-02-04 07:49:33 -08:00 |
|
Leonardo de Moura
|
c763f72b79
|
chore: update stage0
|
2020-02-03 20:25:39 -08:00 |
|
Leonardo de Moura
|
1f359b9844
|
chore: remove unnecessary workaround
It is not needed anymore after we fixed the `app` parser
|
2020-02-03 20:25:09 -08:00 |
|
Leonardo de Moura
|
6be9a73e51
|
chore: update stage0
|
2020-02-03 20:15:00 -08:00 |
|
Leonardo de Moura
|
d75cd49ea2
|
fix: app parser
cc @kha
|
2020-02-03 20:13:38 -08:00 |
|
Leonardo de Moura
|
2138a11480
|
feat: use custom error messages at checkRBPGreater
|
2020-02-03 18:30:22 -08:00 |
|
Leonardo de Moura
|
bf15530c49
|
chore: update stage0
|
2020-02-03 18:21:33 -08:00 |
|
Leonardo de Moura
|
99f7aff491
|
fix: liftMethod notation
|
2020-02-03 17:12:44 -08:00 |
|
Leonardo de Moura
|
31bb6a1dec
|
feat: extend tryCoeAndLift
Add combined coe+lift case.
|
2020-02-03 14:30:13 -08:00 |
|
Leonardo de Moura
|
a75d93b252
|
chore: update stage0
|
2020-02-03 14:13:43 -08:00 |
|
Leonardo de Moura
|
bcfaeaceab
|
feat: change ite and dite argument order
Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.
|
2020-02-03 14:11:29 -08:00 |
|
Leonardo de Moura
|
a474850f5e
|
feat: use automatic liftM at ensureHasType
|
2020-02-03 13:06:36 -08:00 |
|
Leonardo de Moura
|
48acc748ef
|
feat: improve automatic liftM at do blocks
We now don't need to use `decide` in the following example:
```
def pred (x : Nat) : IO Bool := do
pure $ decide $ (← g 1) > 0
```
|
2020-02-03 12:16:57 -08:00 |
|
Leonardo de Moura
|
ba915d90f5
|
feat: do not enable constApprox in the combinator approxDefEq
|
2020-02-03 11:50:40 -08:00 |
|
Leonardo de Moura
|
a134db5e07
|
feat: add Coe instances for monads
|
2020-02-03 11:41:00 -08:00 |
|
Leonardo de Moura
|
330aa59356
|
chore: update stage0
|
2020-02-03 09:49:31 -08:00 |
|
Sebastian Ullrich
|
4279df4170
|
perf: special-case antiquotation syntax in Pratt parser to avoid choice nodes
fixes #99
|
2020-02-03 09:43:41 -08:00 |
|
Leonardo de Moura
|
17cc925115
|
feat: change liftMethod notation
cc @Kha
|
2020-02-03 09:38:05 -08:00 |
|
Sebastian Ullrich
|
fdfbb9a435
|
chore: lean4-mode: remove '.' from symbol table
|
2020-02-03 16:37:02 +01:00 |
|
Sebastian Ullrich
|
b76be34119
|
chore: fix test
|
2020-02-03 16:36:37 +01:00 |
|
Leonardo de Moura
|
f8bfe88d6b
|
fix: consume unnecessary let-decls at isDefEq
Make sure we solve unification constraints such as `(let x := v; ?m) =?= ?m`
|
2020-02-02 21:54:44 -08:00 |
|
Leonardo de Moura
|
2ad065eb93
|
feat: add expandNonAtomicExplicitSource and getStructName
|
2020-02-02 21:24:14 -08:00 |
|
Leonardo de Moura
|
7b1a4272f8
|
chore: update stage0
|
2020-02-02 17:39:35 -08:00 |
|
Leonardo de Moura
|
f40129ad8d
|
fix: precedence
|
2020-02-02 17:37:46 -08:00 |
|
Leonardo de Moura
|
c6b3b1f6f0
|
chore: add StructInst skeleton
|
2020-02-02 17:36:43 -08:00 |
|
Leonardo de Moura
|
4427d4468b
|
feat: add modifyOp
|
2020-02-02 17:30:56 -08:00 |
|
Leonardo de Moura
|
cdb7e0cfae
|
feat: add structInstLVal
|
2020-02-02 17:30:36 -08:00 |
|
Leonardo de Moura
|
2abfa1bcff
|
fix: closes #108
|
2020-02-01 23:17:00 -08:00 |
|
Leonardo de Moura
|
8487216b1e
|
feat: fallback to constApprox when foApprox fails
|
2020-02-01 22:50:29 -08:00 |
|
Leonardo de Moura
|
8de49b157c
|
feat: add new approximation at isDefEq
|
2020-02-01 22:38:58 -08:00 |
|
Leonardo de Moura
|
6252b07735
|
refactor: make sure CheckAssignmentM can use MetaM
|
2020-02-01 21:29:23 -08:00 |
|