diff options
| author | Brian Campbell | 2018-06-04 18:04:45 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | ba3b93c97fa72e05156893d0421a93d4dd5b7fcf (patch) | |
| tree | aae32ab75588b1abf2eb78c02c9bc93cb602c9ff /lib/hol/sail_valuesAuxiliaryScript.sml | |
| parent | 6b485cb062f474454b467c53edff69b10f6d3b5f (diff) | |
Coq: existential and constraint solving work
- 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
Diffstat (limited to 'lib/hol/sail_valuesAuxiliaryScript.sml')
0 files changed, 0 insertions, 0 deletions