Leonardo de Moura
22ae065d16
feat: add { ... : <expected-type> } syntax
...
It replaces the `{ <struct-name> . ... }` syntax.
2020-05-20 15:24:27 -07:00
Leonardo de Moura
bd58048449
chore: { <source> with ... } syntax
2020-05-20 15:08:43 -07:00
Sebastian Ullrich
3d891be49e
feat: delaborator: do not set whitespace information
2020-05-20 11:54:53 -07:00
Sebastian Ullrich
053d4bab1c
chore: factor out and unify common test behavior; retrieve lean from PATH
...
`./test_single.sh foo.lean yes` is now `./test_single.sh -i foo.lean`
2020-05-14 14:38:52 +02:00
Sebastian Ullrich
2325f5d358
chore: ignore more test output files
2020-05-14 14:38:52 +02:00
Leonardo de Moura
ebc0663b3f
chore: fix tests
2020-05-12 15:02:03 -07:00
Sebastian Ullrich
e7920bcdb5
chore: remove test special case
2020-05-04 11:11:11 +02:00
Sebastian Ullrich
8f67db0101
refactor: never implicitly ignore monadic results
...
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
2020-04-23 11:09:59 -07:00
Leonardo de Moura
360cebf680
fix: induction tactic must check expected major premise type
...
`whnfUntil` now returns `Option Expr`.
2020-04-09 11:18:02 -07:00
Leonardo de Moura
9a5bed0f94
fix: missing ! at whnfUntil
2020-04-09 10:49:20 -07:00
Leonardo de Moura
7a5fcfae8b
feat: add [recursor] attribute to Iff.elim
2020-04-09 10:45:27 -07:00
Leonardo de Moura
40336131bb
feat: do not switch to term mode in the RHS of induction and cases tactics
2020-04-08 17:45:06 -07:00
Daniel Selsam
7c1c0dc01e
test: example that requires the instance arg reordering
2020-04-08 16:56:14 -07:00
Leonardo de Moura
e22af8d1ef
feat: add FloatArray
...
cc @dselsam
2020-04-07 18:05:54 -07:00
Leonardo de Moura
b8ea55c989
feat: expose some transcendental functions from the C library
...
cc @dselsam
2020-04-06 15:22:25 -07:00
Leonardo de Moura
8e84a8c9ec
feat: Float from big numbers
2020-04-06 14:05:17 -07:00
Leonardo de Moura
22fc56f5c8
chore: fix test
2020-03-31 10:10:57 -07:00
Leonardo de Moura
af8bc28be0
fix: typo at IR.Expr.alphaEqv
2020-03-31 10:04:59 -07:00
Daniel Selsam
722ea2b694
failing test for suspicious behavior
2020-03-31 10:03:22 -07:00
Sebastian Ullrich
b6fc9428f1
fix: support Windows newlines and '\r' escape
2020-03-27 13:21:21 -07:00
Leonardo de Moura
0595e8a78a
feat: add tryPureCoe
...
@Kha It seems to work reasonably well. It didn't break any test.
2020-03-27 11:20:43 -07:00
Leonardo de Moura
02acdee9ce
feat: disable implicit lambda insertion for fun containing {} or []
...
cc @Kha
2020-03-26 14:32:12 -07:00
Leonardo de Moura
b4b5f2736f
feat: elaborate [] and {} binder annotations in lambda abstractions
...
We can simulate Lean3 behavior.
2020-03-26 14:20:39 -07:00
Leonardo de Moura
07ffa535fe
refactor: decide whether to insert implicit lambdas AFTER macro expansion
...
cc @Kha
2020-03-26 13:53:15 -07:00
Leonardo de Moura
2b3bdbe0cf
test: implicit lambdas + notation
2020-03-26 12:31:04 -07:00
Leonardo de Moura
e682c1c88f
fix: make sure @ disable new syntax and macros too
...
cc @Kha
2020-03-26 12:14:55 -07:00
Leonardo de Moura
6625656940
refactor: remove support for fun {a : A} => ...
...
The semantics was weird. It seems Agda is also having problems with
it. Here is an example that demonstrates how weird the semantics is:
```lean
check (fun {β α} (a : α) (b : β) => (b, a) : {α : Type} → {β : Type} → (a : α) → (b : β) → β × α)
-- Same example using `def`
def f : {α : Type} → {β : Type} → α → β → β × α :=
fun {β : Type} {α : Type} (a : α) (b : β) => (b, a)
```
Both commands were being accepted before this commit. Note that it
flips `β` and `α`.
Here is an example that did not work before this commit and would
confuse users.
```lean
check
let id := fun {α} (a : α) => a;
id [id 1]
```
users would have to write
```lean
check
let id {α} (a : α) := a;
id [id 1]
```
@Kha The Delaborator.lean test broke and I "fixed" by removing the
`{}` from it, and copying `produced` over `expected`. Please make sure
it still makes sense.
2020-03-26 10:40:16 -07:00
Leonardo de Moura
d79cfa38e3
test: generalizeTelescope tests
2020-03-25 16:00:55 -07:00
Leonardo de Moura
2ca347fcd6
chore: fix test
2020-03-23 15:47:51 -07:00
Leonardo de Moura
dc80b76106
feat: add IO.FS.lines
2020-03-23 14:53:27 -07:00
Leonardo de Moura
94f016a3e8
fix: readLine and test
2020-03-23 14:06:17 -07:00
Leonardo de Moura
db914052ce
fix: IO.getLine
2020-03-23 12:26:09 -07:00
Leonardo de Moura
4296e1d83e
feat: add tests for Closure.lean
2020-03-20 18:32:04 -07:00
Leonardo de Moura
eaaaaabc60
feat: allow Lean.Parser.Term.id to be used in binders
...
cc @Kha
2020-03-18 20:54:08 -07:00
Leonardo de Moura
2954f6ad3e
feat: add MetaHasEval instance for TermElabM
...
cc @Kha
2020-03-18 20:09:14 -07:00
Leonardo de Moura
5d35b2c419
test: decide! tests
2020-03-18 16:48:28 -07:00
Leonardo de Moura
736925bbce
feat: allow decide! and nativeDecide! take _ as an argument
...
We use the expected type in this case.
2020-03-18 16:00:06 -07:00
Leonardo de Moura
c8b51b0fb3
feat: elab decide!
2020-03-18 15:48:22 -07:00
Leonardo de Moura
5b350d52ee
feat: elaborate nativeDecide!
2020-03-18 15:39:23 -07:00
Leonardo de Moura
bfe7d1ffe8
chore: add kernel WHNF test
2020-03-18 11:07:24 -07:00
Leonardo de Moura
6f62986368
feat: add isDefEqStringLit
2020-03-18 11:05:44 -07:00
Leonardo de Moura
cee478dc94
feat: MetaM support for expanding String literal at recursors
2020-03-18 10:29:52 -07:00
Leonardo de Moura
b4942fcd30
feat: add ToExpr instances
2020-03-18 10:22:24 -07:00
Leonardo de Moura
72ec0ec3ad
feat: string literal support on recursors and kernel isDefEq
2020-03-17 17:23:33 -07:00
Leonardo de Moura
78b5e714c5
test: add rfl tests
2020-03-17 16:18:18 -07:00
Leonardo de Moura
3df7f35dd0
test: kernel isDefEq support for Nat operations
2020-03-17 13:38:06 -07:00
Leonardo de Moura
7a82318d37
fix: to_pattern_fn bug
2020-03-17 12:58:08 -07:00
Leonardo de Moura
97b8d8551d
feat: elaborate nativeRefl! macro
2020-03-16 16:21:51 -07:00
Leonardo de Moura
acee5719af
test: proofs by reflection
2020-03-16 14:33:30 -07:00
Leonardo de Moura
b69c851a5a
feat: add Expr.foldConsts
2020-03-16 14:33:30 -07:00
