Sebastian Ullrich
30f4b2f2dd
refactor(library): list.taken/dropn ~> list.take/drop
2017-07-05 11:20:10 -07:00
Leonardo de Moura
cfa34dc83e
chore(library): remove workarounds for issue #1682
2017-06-19 16:09:12 -07:00
Leonardo de Moura
b8fa7f5311
fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean
...
See #1664
2017-06-18 18:33:27 -07:00
Leonardo de Moura
049fecee23
fix(library/init): name has_repr instance is actually a has_to_string instance
...
See #1664
2017-06-18 18:33:16 -07:00
Leonardo de Moura
dc1a1c8540
refactor(library): has_to_string ==> has_repr
...
See issue #1664
This is just the first step to implement proposal described at issue #1664 .
2017-06-18 18:29:19 -07:00
Sebastian Ullrich
808ab73d93
refactor(init): use list for expr.macro args
2017-05-14 19:17:28 -07:00
Leonardo de Moura
f6b47ea5c7
feat(library/init/category): add has_map type class, delete fmap
2017-05-01 10:13:02 -07:00
Leonardo de Moura
ad859817b1
feat(frontends/lean): allow local decls to shadow namespaces
2017-03-29 16:09:45 -07:00
Leonardo de Moura
1cdf13821c
feat(library/init/data/unsigned): add basic unsigned operations
2017-03-05 16:14:16 -08:00
Leonardo de Moura
552a185e6a
feat(frontends/lean): 'let' in 'do' blocks
2017-02-24 09:10:36 -08:00
Leonardo de Moura
edd5e97045
feat(frontends/lean/elaborator): coercion from (decidable) Prop to bool
...
This is a hard coded extra case. It is not an instance of has_coe.
Even if we change has_coe to accomodate this case, it will not be a
satisfactory solution because this coercion depends on the element and
not the type, and the element usually contains metavariables.
We should eventually write a tactic for synthesizing coercions.
2017-02-14 18:41:32 -08:00
Leonardo de Moura
6e7929252f
feat(frontends/lean, library/init): add 'thunk' gadget
...
We can now write
trace "hello" t
instead of
trace "hello" (fun _, t)
2017-01-31 18:41:59 -08:00
Leonardo de Moura
bf9f7560f7
feat(frontends/lean): (Type u) can't be a proposition
...
(Type u) is the old (Type (u+1))
(PType u) is the old (Type u)
Type* is the old (Type (_+1))
PType* is the old Type*
The stdlib can be compiled, but we still have > 70 broken tests
See discussion at #1341
2017-01-30 11:54:00 -08:00
Jared Roesch
e65d90ac79
feat(*): C++ code generator
...
in progress move of Lean.native to init
2016-12-05 16:11:41 -08:00
