Leonardo de Moura
8e84a8c9ec
feat: Float from big numbers
2020-04-06 14:05:17 -07:00
Sebastian Ullrich
f66039f7f0
feat: generalize Array function universes
2020-04-06 13:48:09 -07:00
Leonardo de Moura
746615d81d
chore: remove ⇒ as alternative for =>
2020-04-06 13:45:22 -07:00
Sebastian Ullrich
729c750003
doc: adjust commit convention
...
/cc @leodemoura
2020-04-05 11:29:30 +02:00
Sebastian Ullrich
e971c8dd7a
feat: support Float in the interpreter
...
/cc @leodemoura @dselsam
2020-04-05 10:50:30 +02:00
Leonardo de Moura
03f0c3fdd8
chore: update stage0
2020-04-03 18:28:35 -07:00
Leonardo de Moura
acad6015c4
chore: add new primitives to object.h
2020-04-03 18:26:13 -07:00
Leonardo de Moura
582fe3ac8a
test: add test that exposed unboxing issue
2020-04-03 18:24:48 -07:00
Leonardo de Moura
64c3be44f8
fix: lean_unbox_float
2020-04-03 18:23:45 -07:00
Leonardo de Moura
8e952f3c36
chore: style
2020-04-03 17:48:06 -07:00
Leonardo de Moura
d1b0bd0c77
chore: update stage0
2020-04-03 17:41:09 -07:00
Leonardo de Moura
51f1893a8c
test: add basic float tests
2020-04-03 17:39:47 -07:00
Leonardo de Moura
485034bbba
fix: bug at ir.cpp
2020-04-03 17:39:28 -07:00
Leonardo de Moura
a84c177cb5
chore: update stage0
2020-04-03 17:21:03 -07:00
Leonardo de Moura
c236a179f2
feat: enable externs
2020-04-03 17:19:48 -07:00
Leonardo de Moura
0457cb35ec
chore: update stage0
2020-04-03 17:08:25 -07:00
Leonardo de Moura
0e2ebd36ff
feat: make sure Float is in WHNF
2020-04-03 17:07:29 -07:00
Leonardo de Moura
c6d77423d1
chore: update stage0
2020-04-03 16:51:39 -07:00
Leonardo de Moura
b5f258773b
feat: add Float
2020-04-03 16:49:32 -07:00
Leonardo de Moura
60d84660e6
feat: add support for Float in the compiler
2020-04-03 16:39:29 -07:00
Leonardo de Moura
b0a02ef0bb
feat: emit float runtime primitives
2020-04-03 16:02:35 -07:00
Leonardo de Moura
71397aad36
feat: runtime primitives
2020-04-03 15:55:39 -07:00
Leonardo de Moura
52cffcb67f
feat: add Float.lean
2020-04-03 15:40:38 -07:00
Leonardo de Moura
3dda98a40b
proto: checkpoint
2020-04-03 15:20:54 -07:00
Leonardo de Moura
22fc56f5c8
chore: fix test
2020-03-31 10:10:57 -07:00
Leonardo de Moura
082b13456c
chore: update stage0
2020-03-31 10:06:34 -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
Leonardo de Moura
73f5801d8a
proto: use generalizeTelescope
2020-03-30 11:47:03 -07:00
Leonardo de Moura
0cbd09f967
chore: make sure generalizeTelescope signature is similar to other telescope methods
2020-03-30 11:43:41 -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
3c699eb915
feat: add mkAppOptM
2020-03-27 11:14:38 -07:00
Sebastian Ullrich
fcdbdeecaf
feat: delaborator: use implicit lambdas where possible
...
/cc @leodemoura it's not bullet-proof (unless `pp.explicit` is set), but let's
see if it is good enough in practice
2020-03-27 14:55:46 +01:00
Sebastian Ullrich
db93638a96
feat: delab forallE
2020-03-27 11:59:58 +01:00
Sebastian Ullrich
f39ea47376
chore: brackted ~> bracketed
2020-03-27 10:42:36 +01:00
Sebastian Ullrich
a79a2888d0
refactor: simplify delabLamAux
2020-03-27 10:42:36 +01: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
cda2cdaa60
chore: update stage0
2020-03-26 14:16:00 -07:00
Leonardo de Moura
34ec66edb2
chore: re-enable {} and [] annotations at fun
2020-03-26 14:15:07 -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
0c5a08a16e
chore: make sure Delaborator.lean still compiles
...
@Kha I removed `{}` `[]` from `funBinder`.
Please make sure `Delaborator.lean` still does what you want.
2020-03-26 10:40:16 -07:00
Leonardo de Moura
8c5ac07f81
chore: update stage0
2020-03-26 10:40:16 -07:00
Leonardo de Moura
19be2a5ade
chore: remove {} and [] from funBinder
2020-03-26 10:40:16 -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
Sebastian Ullrich
9be3abd721
doc: update lean4-mode readme
2020-03-26 11:24:01 +01:00
Leonardo de Moura
227f985f84
fix: bug at generalizeTelescope
2020-03-25 16:00:55 -07:00
