From 7f384e7b8964339832921ab65c1d75a4db076ecb Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Fri, 5 Apr 2024 05:36:59 +0000
Subject: [PATCH] GarageDoorTop: assert some types

---
 src/Bedrock/End2End/X25519/GarageDoorTop.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v
index a209f776f0..92c1442569 100644
--- a/src/Bedrock/End2End/X25519/GarageDoorTop.v
+++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v
@@ -258,6 +258,11 @@ Import bedrock2.Map.Separation. Local Open Scope sep_scope.
 Require Import bedrock2.ReversedListNotations.
 Local Notation run1 := (mcomp_sat (run1 Decode.RV32IM)).
 Local Notation RiscvMachine := MetricRiscvMachine.
+Goal True.
+  pose (run1 : RiscvMachine -> (RiscvMachine -> Prop) -> Prop).
+  pose (always(iset:=Decode.RV32IM) : (RiscvMachine -> Prop) -> RiscvMachine -> Prop).
+Abort.
+
 Implicit Types mach : RiscvMachine.
 Local Coercion word.unsigned : word.rep >-> Z.