michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
2368 commits 3 branches 0 tags 28 MiB
Commit graph

13 commits

Author SHA1 Message Date
Leonardo de Moura
eb046c11fb refactor(kernel): the type in let-exprs is not optional anymore, if the user does not provide it, we use a metavariable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:55 -07:00
Leonardo de Moura
9fb3ccb4c0 feat(library/simplifier): support for dependent simplification in lambda expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 16:54:42 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression 
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-07 23:21:10 -08:00
Leonardo de Moura
0390f3c39b feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-12-06 15:01:54 -08:00
Soonho Kong
5c3866cd71 Use fullpath in #include directives, add missing STL headers 2013-09-13 03:35:29 -07:00
Leonardo de Moura
2459c4ae7c Add (optional) type to let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-09-06 10:06:26 -07:00
Leonardo de Moura
984c4149fa Add helper functions for creating Let expressions. Add simple type checking test for Let expressions. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-14 22:30:12 -07:00
Leonardo de Moura
3d9f9a12d1 Enable automatic coercion from 'char const *' to hierachical name 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-10 14:21:13 -07:00
Leonardo de Moura
84f4a32c0e Change name convention for creating Lean expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-06 11:27:14 -07:00
Leonardo de Moura
30513398bb Add basic definitions and axioms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-05 20:06:42 -07:00
Leonardo de Moura
cce469119f Flip order of the arguments for instance and abstract. Simplify type_checker. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-03 16:12:15 -07:00
Leonardo de Moura
3ef9d21875 Fix bugs in type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-08-01 21:40:39 -07:00
Leonardo de Moura
9b3c47a521 Refactor instantiate/abstract code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-07-24 14:56:32 -07:00