From 1db7e1c63d2d8ee9c3c45ac4494c1bfaf96e68d6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 18 Apr 2018 16:09:44 +0100
Subject: Add first draft of Isabelle library documentation

---
 src/state.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3