diff options
| author | Thomas Bauereiss | 2018-04-18 16:09:44 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-04-18 16:31:51 +0100 |
| commit | 1db7e1c63d2d8ee9c3c45ac4494c1bfaf96e68d6 (patch) | |
| tree | e54fa6fa87b8eff295591277c4b6867c619b0b2e /src | |
| parent | 1dd0317817fcd143bea33bba4cfc15f5242210b5 (diff) | |
Add first draft of Isabelle library documentation
Diffstat (limited to 'src')
| -rw-r--r-- | src/state.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/state.ml b/src/state.ml index 40ec80ad..59fb9995 100644 --- a/src/state.ml +++ b/src/state.ml @@ -242,6 +242,9 @@ let register_refs_lem mwords registers = in separate hardline [generic_convs; refs; getters_setters] +(* TODO Generate well-typedness predicate for register states (and events), + asserting that all lists representing non-bit-vectors have the right length. *) + let generate_isa_lemmas mwords (Defs defs : tannot defs) = let rec drop_while f = function | x :: xs when f x -> drop_while f xs |