Leonardo de Moura
|
c41667bf13
|
feat(library/init): mark Prod, Except, Sigma and Option with [unbox]
|
2019-10-02 16:50:37 -07:00 |
|
Leonardo de Moura
|
128acd3b47
|
chore(library/init): remove @[extern cpp ...]
|
2019-08-24 07:40:38 -07:00 |
|
Leonardo de Moura
|
98e6e0c09a
|
feat(library/init): add "extern c" attributes
|
2019-08-20 11:53:46 -07:00 |
|
Leonardo de Moura
|
d00019f57e
|
chore(library/init): fix whitspaces before =>
|
2019-08-09 09:13:49 -07:00 |
|
Leonardo de Moura
|
4d913370a7
|
chore(library/init): eliminate whitespaces using another patch script
|
2019-08-09 09:01:39 -07:00 |
|
Sebastian Ullrich
|
3ed67138d5
|
chore(*): update equation syntax in files and old parser
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
|
2019-08-09 11:11:34 +02:00 |
|
Leonardo de Moura
|
b221b09ad5
|
chore(library/init, frontends/lean): ensure old and new parser use the same command for initializing quotient module
|
2019-07-31 17:07:05 -07:00 |
|
Leonardo de Moura
|
6711b45d92
|
chore(library/init/core): missing parentheses
|
2019-07-15 16:05:12 -07:00 |
|
Leonardo de Moura
|
070fe8c00a
|
chore(library/init/core): avoid unnecessary notation
Motivation: simplify transition to new parser.
|
2019-07-12 14:24:46 -07:00 |
|
Leonardo de Moura
|
d7a60c0b7f
|
chore(library/init): temporarily disable unquoted symbols
|
2019-07-12 14:07:33 -07:00 |
|
Leonardo de Moura
|
7c53be5df7
|
chore(library/init): remove remaining set notation
|
2019-07-11 10:31:25 -07:00 |
|
Leonardo de Moura
|
295cabed2e
|
chore(library/init): remove unnecessary notations
|
2019-07-11 10:27:16 -07:00 |
|
Leonardo de Moura
|
57e2f1be2a
|
feat(library/init/lean/parser/term): builtin operators
|
2019-07-11 10:13:00 -07:00 |
|
Leonardo de Moura
|
1a81d60820
|
chore(frontends/lean/parser): simplify binder notation
The `<ident> : <expr>` now requires explicit brackets.
|
2019-07-08 08:54:19 -07:00 |
|
Leonardo de Moura
|
3285a9e77d
|
chore(library/init): unnecessary parentheses
|
2019-07-05 13:23:19 -07:00 |
|
Leonardo de Moura
|
ea6eee516b
|
chore(frontends/lean): use => instead of := in match-expressions
Motivation: use same separator used in lambda expressions as in
other programming languages.
|
2019-07-04 11:38:38 -07:00 |
|
Leonardo de Moura
|
df9b8feef6
|
chore(library/init/core): minor
|
2019-07-02 17:37:35 -07:00 |
|
Leonardo de Moura
|
07cff06b6e
|
chore(library): Π ==> ∀
|
2019-07-02 17:35:15 -07:00 |
|
Leonardo de Moura
|
f74f5bc33a
|
fix(library/init/core): show
|
2019-07-02 17:27:03 -07:00 |
|
Leonardo de Moura
|
0bee94886e
|
feat(frontends/lean/builtin_exprs): , from ==> from, and cleanup suffices
|
2019-07-02 17:22:50 -07:00 |
|
Leonardo de Moura
|
7ba9a5012a
|
chore(frontends/lean/builtin_exprs): make sure have-expression is consistent with let-expression
|
2019-07-02 16:46:51 -07:00 |
|
Leonardo de Moura
|
a02443d23d
|
chore(frontends/lean): fun x, e ==> fun x => e
|
2019-07-02 13:22:11 -07:00 |
|
Leonardo de Moura
|
39221adcd6
|
chore(frontends/lean/builtin_exprs): remove assume notation
|
2019-07-02 10:40:07 -07:00 |
|
Leonardo de Moura
|
300414e6e4
|
chore(frontends/lean): change explicit universe parameter notation in declarations
|
2019-07-02 08:57:08 -07:00 |
|
Leonardo de Moura
|
ab487ea4ac
|
feat(frontends/lean): allow ; instead of in in let-decls
|
2019-06-27 17:12:03 -07:00 |
|
Leonardo de Moura
|
9f358649ec
|
feat(library/init/core): avoid [macroInline] + [inline] in same declaration
It will be rejected in the future.
|
2019-06-26 13:54:58 -07:00 |
|
Leonardo de Moura
|
e00dc873a8
|
chore(library/pattern_attribute): [pattern] ==> [matchPattern]
|
2019-06-26 11:26:49 -07:00 |
|
Leonardo de Moura
|
714468dc60
|
chore(frontends/lean): remove include and omit commands
|
2019-06-24 15:48:11 -07:00 |
|
Leonardo de Moura
|
af2d6dbd45
|
chore(library/init): avoid local attribute
|
2019-06-24 15:48:11 -07:00 |
|
Leonardo de Moura
|
94bca2b9d8
|
chore(library/init): mimize use of notations
|
2019-06-24 15:48:11 -07:00 |
|
Leonardo de Moura
|
dda0e38802
|
chore(library/init): avoid local notation
|
2019-06-24 15:48:11 -07:00 |
|
Leonardo de Moura
|
4ab31275a4
|
chore(library/init, frontends/lean): remove foldl and foldr notation, and implement list notation in the old parser
|
2019-06-20 14:32:08 -07:00 |
|
Leonardo de Moura
|
9e73d92e42
|
chore(library/init): remove instances of scoped notation
|
2019-06-20 14:08:35 -07:00 |
|
Leonardo de Moura
|
00aa2a3ffe
|
chore(library/user_recursors): remove [recursor] attribute and environment extension
|
2019-06-20 11:25:53 -07:00 |
|
Leonardo de Moura
|
1e30f76511
|
chore(frontends/lean/pp): remove ppAsAnonymousCtor attribute
|
2019-06-20 11:03:20 -07:00 |
|
Leonardo de Moura
|
0b99a18f97
|
chore(library): use >> as notation for andthen
We have other plans for `;`.
|
2019-06-20 09:54:53 -07:00 |
|
Leonardo de Moura
|
f5725abb57
|
refactor(library/init/lean/environment): cleanup and improve
|
2019-05-10 15:54:29 -07:00 |
|
Leonardo de Moura
|
20285b1079
|
fix(library/init/core): incorrectly fixing universe level at 1
|
2019-05-06 18:20:39 -07:00 |
|
Leonardo de Moura
|
0d1a0c8b6e
|
chore(library): toBool ==> decide
We want to define a type class similar to Haskell's `ToBool`.
|
2019-05-06 14:02:15 -07:00 |
|
Leonardo de Moura
|
82d88dc96f
|
chore(library/init/core): make sure new frontend can parse it
@kha This is a temporary fix. We will get back to the new frontend after
we submit the IR paper.
|
2019-05-03 17:36:39 -07:00 |
|
Sebastian Ullrich
|
c77970a00f
|
refactor(library): remove now-redundant parentheses
|
2019-05-03 13:57:21 +02:00 |
|
Leonardo de Moura
|
abaf181495
|
refactor(core): homogeneous andthen
The motivation is to make sure `andthen` and `orelse` are both
homogeneous.
|
2019-04-24 14:00:34 -07:00 |
|
Leonardo de Moura
|
2cd3954198
|
chore(library/init/core): remove misleading annotation
The compiler will not try to inline definitions tagged as `@[extern]`.
`strictOr` and `strictAnd` must be handled using the constant folding module.
|
2019-04-05 16:29:44 -07:00 |
|
Leonardo de Moura
|
5f6106be83
|
chore(init): add reserve for all control notation at core.lean
cc @kha
|
2019-04-04 08:53:42 -07:00 |
|
Leonardo de Moura
|
5b31f85fcb
|
chore(library/init/core): add extern for strictAnd and strictOr
|
2019-03-30 08:04:16 -07:00 |
|
Sebastian Ullrich
|
21f1d231b8
|
fix(runtime/object): do not return temporary borrowed reference from a builtin
|
2019-03-29 14:32:15 +01:00 |
|
Leonardo de Moura
|
2943fce8c8
|
chore(library/init/core): add strictAnd and strictOr
|
2019-03-28 09:42:12 -07:00 |
|
Leonardo de Moura
|
9a071c18e7
|
feat(library/equations_compiler): add support for partial definitions
|
2019-03-27 11:09:32 -07:00 |
|
Leonardo de Moura
|
2a37e60ba9
|
feat(library/init/core): add != notation
|
2019-03-25 16:58:01 -07:00 |
|
Leonardo de Moura
|
3ad7d2ba81
|
fix(library/compiler/lcnf): disable transformation for Bool
@kha Here is another motivation for re-implementing the equation compiler.
|
2019-03-25 16:48:11 -07:00 |
|