Commit graph

6 commits

Author SHA1 Message Date
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
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
190855ad1b Add (relaxed) version of instantiate that can substitute terms containing free variables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-03 16:12:15 -07:00
Leonardo de Moura
1398c927cd Fix compilation error with clang++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-24 14:56:32 -07:00
Leonardo de Moura
4b61639f4d Use consistent naming for functional objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-07-24 14:56:32 -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