diff options
Diffstat (limited to 'src/BoundedArithmetic/InterfaceProofs.v')
| -rw-r--r-- | src/BoundedArithmetic/InterfaceProofs.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/BoundedArithmetic/InterfaceProofs.v b/src/BoundedArithmetic/InterfaceProofs.v index 8256fc23f..25cd09e85 100644 --- a/src/BoundedArithmetic/InterfaceProofs.v +++ b/src/BoundedArithmetic/InterfaceProofs.v @@ -12,6 +12,9 @@ Local Open Scope Z_scope. Import BoundedRewriteNotations. Local Notation bit b := (if b then 1 else 0). +Lemma decoder_eta {n W} (decode : decoder n W) : decode = {| Interface.decode := decode |}. +Proof. destruct decode; reflexivity. Defined. + Section InstructionGallery. Context (n : Z) (* bit-width of width of [W] *) {W : Type} (* bounded type, [W] for word *) |