Leonardo de Moura
|
4c19cc6957
|
Rename lean frontend files. The prefix lean_ is not necessary anymore.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-12 20:09:35 -07:00 |
|
Leonardo de Moura
|
26097475fd
|
Use fullpath in #include directives.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-12 20:04:10 -07:00 |
|
Leonardo de Moura
|
c674bb3790
|
Add castlib as an independent library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 23:40:47 -07:00 |
|
Leonardo de Moura
|
7a9d53d0d7
|
Refactor arith libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 23:19:47 -07:00 |
|
Leonardo de Moura
|
c0c2f52087
|
Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-06 18:32:15 -07:00 |
|
Leonardo de Moura
|
fc9e395818
|
Define absolute value function and notation for it. Add new example.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-03 20:39:54 -07:00 |
|
Leonardo de Moura
|
3992c4b8f9
|
Define divides, and add examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-03 20:18:20 -07:00 |
|
Leonardo de Moura
|
e031d7bc10
|
Improve error messages when overloads+coercions do not work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-02 20:05:47 -07:00 |
|
Leonardo de Moura
|
395513258e
|
Define mod and unary minus
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-02 16:31:44 -07:00 |
|
Leonardo de Moura
|
abc939382b
|
Add Real arithmetic. Fix elaborator for coercions. Now, two overloads are considered ambiguous if they need the same number of coercions. Improve pretty printer for nest infix operators with same precedence and associativity.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-02 13:20:00 -07:00 |
|
Leonardo de Moura
|
0a67679afb
|
Add natural numbers. Fix how coercions and overloads interact (switch to approach used in C++). Add notation for natural and integer arithmetic. Rename m and u universe variables to M and U.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-09-02 12:24:29 -07:00 |
|
Leonardo de Moura
|
1b6d51b0aa
|
Mark implicit arguments of builtin symbols
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-30 15:56:04 -07:00 |
|
Leonardo de Moura
|
4ef4655183
|
Add homogeneous equality
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-30 14:26:12 -07:00 |
|
Soonho Kong
|
3f40953efc
|
Add comments for unicode symbols, fix a typo
|
2013-08-21 14:35:45 -07:00 |
|
Leonardo de Moura
|
d750469667
|
Move frontend to frontends/lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-08-21 09:04:49 -07:00 |
|