| Age | Commit message (Collapse) | Author |
|---|
|
|
|
(The last bit is to declare type aliases as Type so that Coq uses the
type scope for notation, so * is prod, not multiplication).
|
|
Plus
- Complete solver support for inequalities
- Reduce exponentials in solver
|
|
|
|
- add existential unpacking for function arguments
- add mechanism for using properties for existentially typed top-level
values (useful for the typechecking tests)
- support for length_list and In in Coq constraint solving
|
|
Only single variable in places, only packed at literals and variables,
no unpacking
|
|
vector_access is a bit hacky at the moment - it expects a constraint to
be shown between the index and the list size, but we don't track list
sizes in general
|
|
|
|
|
