Leonardo de Moura
|
80cf1e8353
|
feat(library/metavar_context): use head_beta_reduce at mk_metavar_decl
|
2016-07-05 13:50:44 -07:00 |
|
Leonardo de Moura
|
61a845c005
|
feat(library/tactic): add 'apply' tactic
|
2016-06-17 20:11:52 -07:00 |
|
Leonardo de Moura
|
26c10c368a
|
refactor(library): instantiate ==> instantiate_mvars
Motivation: avoid confusion with 'instantiate' procedure for variables
|
2016-06-14 10:29:47 -07:00 |
|
Leonardo de Moura
|
4c6de9f8e4
|
fix(library/metavar_context): incorrect assertions
|
2016-06-11 20:29:10 -07:00 |
|
Leonardo de Moura
|
8038ca5f0c
|
refactor(metavar_context): metavar_decl contains a local_context instead of local_decls
Motivations:
- A goal is essentially a metavar_decl
- We need the local_context to implement restrict_metavars_context method
|
2016-03-15 12:52:30 -07:00 |
|
Leonardo de Moura
|
9ecd4a2c85
|
dec(library/type_context): basic backtracking support
|
2016-03-13 13:22:48 -07:00 |
|
Leonardo de Moura
|
011b388247
|
feat(library): add metavar_util template to avoid code duplication
|
2016-03-10 14:07:57 -08:00 |
|
Leonardo de Moura
|
ea2d3de71b
|
dev(library/type_context): is_def_eq for universes
|
2016-03-10 12:13:32 -08:00 |
|
Leonardo de Moura
|
c0fc9e5479
|
feat(library/local_context, library/metavar_context): add new well_formed methods and procedures
|
2016-03-05 14:56:13 -08:00 |
|
Leonardo de Moura
|
4543dc4a7f
|
feat(library): add metavar_context
|
2016-03-05 12:53:45 -08:00 |
|