Leonardo de Moura
|
98c925ed7e
|
feat: elaborate #check_failure
|
2020-02-12 11:55:02 -08:00 |
|
Leonardo de Moura
|
17dfe3fb66
|
test: implicit lambda tests
|
2020-02-11 21:21:21 -08:00 |
|
Leonardo de Moura
|
41baf46083
|
feat: propagate expected type at elabFunCore
|
2020-02-11 17:47:51 -08:00 |
|
Leonardo de Moura
|
97dfe95b41
|
chore: fix test
and document why better expected type propagation broke this example.
|
2020-02-11 16:26:39 -08:00 |
|
Leonardo de Moura
|
2f959e23ca
|
fix: checkAssignment was overwriting assignment
|
2020-02-11 16:11:56 -08:00 |
|
Leonardo de Moura
|
55231b960e
|
feat: simplify and improve processAssignmentFOApproxAux
|
2020-02-11 14:42:02 -08:00 |
|
Leonardo de Moura
|
30e0ccd8c4
|
feat: implicit lambdas
It is still work in progress
|
2020-02-11 13:43:05 -08:00 |
|
Leonardo de Moura
|
03b5b7d562
|
feat: implicit lambdas
|
2020-02-11 09:59:46 -08:00 |
|
Leonardo de Moura
|
adb940e879
|
feat: new test
|
2020-02-11 09:34:45 -08:00 |
|
Leonardo de Moura
|
7085072590
|
feat: allow implicitBinder and instBinder at fun
|
2020-02-11 08:26:10 -08:00 |
|
Leonardo de Moura
|
f6ae8560e8
|
fix: isDefEq issue exposed by new test
|
2020-02-10 23:46:17 -08:00 |
|
Leonardo de Moura
|
f39586a237
|
test: expose problem at isDefEq
|
2020-02-10 22:22:42 -08:00 |
|
Leonardo de Moura
|
e732eac899
|
fix: but at elimMVarDepsApp
|
2020-02-10 20:49:43 -08:00 |
|
Leonardo de Moura
|
f0e2a3cfa4
|
chore: add small test
|
2020-02-10 20:37:37 -08:00 |
|
Leonardo de Moura
|
34776c4f41
|
chore: fix test
|
2020-02-10 14:48:57 -08:00 |
|
Leonardo de Moura
|
c3b2a1da50
|
fix: bug at subst tactic
|
2020-02-09 19:25:15 -08:00 |
|
Leonardo de Moura
|
352b720728
|
test: add clear failure test
|
2020-02-09 16:48:36 -08:00 |
|
Leonardo de Moura
|
22ff3c7db2
|
feat: add evalClear
|
2020-02-09 16:41:29 -08:00 |
|
Leonardo de Moura
|
95ad26cc23
|
feat: add mkEqNDRec and mkEqRec
|
2020-02-09 11:02:35 -08:00 |
|
Leonardo de Moura
|
7c7c4edf38
|
feat: add evalRevert
|
2020-02-08 18:51:11 -08:00 |
|
Leonardo de Moura
|
3c5b3cd91f
|
feat: add Expr.replace helper function
|
2020-02-06 14:03:54 -08:00 |
|
Leonardo de Moura
|
eacff1a448
|
feat: implement withPtrEq and withPtrAddr
|
2020-02-04 17:48:11 -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
|
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 |
|
Sebastian Ullrich
|
52a0a0937e
|
feat: check precedence of leading parsers as well
|
2020-02-04 07:49:33 -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
|
d75cd49ea2
|
fix: app parser
cc @kha
|
2020-02-03 20:13:38 -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
|
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
|
17cc925115
|
feat: change liftMethod notation
cc @Kha
|
2020-02-03 09:38:05 -08: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
|
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
|
a7c8978d81
|
feat: insert liftM automatically in do notation when needed
@Kha The new example demonstrates the feature in action.
I added a comment explaining why it is more effective than relying on coercions.
|
2020-02-01 17:33:04 -08:00 |
|
Leonardo de Moura
|
cd4ec6313e
|
chore: try macros first
|
2020-02-01 00:53:49 -08:00 |
|
Leonardo de Moura
|
d8c738bef8
|
feat: elaborate do notation
|
2020-01-31 20:11:06 -08:00 |
|
Leonardo de Moura
|
3d0bfcd36a
|
fix: assertion violation
|
2020-01-31 08:25:59 -08:00 |
|
Leonardo de Moura
|
21618361b7
|
refactor: remove ParserKind
|
2020-01-30 20:56:46 -08:00 |
|
Leonardo de Moura
|
3f32d9eb0b
|
fix: closes #111
|
2020-01-30 14:09:47 -08:00 |
|
Leonardo de Moura
|
2f0ac98b51
|
feat: extend scope of cdot notation
|
2020-01-30 11:42:37 -08:00 |
|
Leonardo de Moura
|
38cfa1dcb6
|
feat: add elabMatch skeleton
|
2020-01-30 10:02:15 -08:00 |
|