| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Base.v | 216 | logplain |
| -rw-r--r-- | Hoare.v | 45136 | logplain |
| -rw-r--r-- | Impl_base.v | 40310 | logplain |
| -rw-r--r-- | Instr_kinds.v | 12942 | logplain |
| -rw-r--r-- | Makefile | 1148 | logplain |
| -rw-r--r-- | Operators.v | 9889 | logplain |
| -rw-r--r-- | Operators_bitlists.v | 6551 | logplain |
| -rw-r--r-- | Operators_mwords.v | 24998 | logplain |
| -rw-r--r-- | Prompt.v | 11905 | logplain |
| -rw-r--r-- | Prompt_monad.v | 17165 | logplain |
| -rw-r--r-- | Real.v | 2766 | logplain |
| -rw-r--r-- | State.v | 9319 | logplain |
| -rw-r--r-- | State_lemmas.v | 47047 | logplain |
| -rw-r--r-- | State_lifting.v | 3442 | logplain |
| -rw-r--r-- | State_monad.v | 15541 | logplain |
| -rw-r--r-- | State_monad_lemmas.v | 22488 | logplain |
| -rw-r--r-- | String.v | 7571 | logplain |
| -rw-r--r-- | Values.v | 97709 | logplain |
| -rw-r--r-- | Values_lemmas.v | 15812 | logplain |
| -rw-r--r-- | _CoqProject | 39 | logplain |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |