Package m0-decomp: M0 decompilation support
Information
| name | m0-decomp |
| version | 1.0 |
| description | M0 decompilation support |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | 1592e8758c119cab52c74a92fdb786115a02af9a |
| requires | base m0-prog |
| show | Data.Bool Data.Pair HOL4 |
Files
- Package tarball m0-decomp-1.0.tgz
- Theory source file m0-decomp.thy (included in the package tarball)
Defined Constant
- HOL4
- m0_decomp
- m0_decomp.m0_COUNT
- m0_decomp
Theorem
⊦ ∀count.
m0_decomp.m0_COUNT count =
set_sep.STAR (m0_prog.m0_count count) (m0_prog.m0_CONFIG (⊥, ⊥))
External Type Operators
- →
- bool
- Data
- Pair
- ×
- Pair
- HOL4
- m0_prog
- m0_prog.m0_component
- m0_prog.m0_data
- m0_prog
- Number
- Natural
- Number.Natural.natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ⊥
- ⊤
- Pair
- ,
- Bool
- HOL4
- m0_prog
- m0_prog.m0_CONFIG
- m0_prog.m0_count
- set_sep
- set_sep.STAR
- m0_prog
Assumptions
⊦ ⊤
⊦ (∀) = λP. P = λx. ⊤