blob: 64c5bf10527ad9ccb2264c69e3897a63e41cb533 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import Sail2_state_monad.
Require Import Sail2_state_lifting.
Require Import String.
Require Import List.
Import ListNotations.
Goal True.
let result := eval cbv in (liftState register_accessors (main tt) (init_state tt)) in
match result with
| [(Value tt,_)] => idtac "OK"
| [(Ex (Failure ?s),_)] => idtac "Fail:" s
| _ => idtac "Fail"
end.
exact I.
Qed.
|
