small change

reilabs · Dec 26, 2024 · 0a0717a · 0a0717a
1 parent 6e1e027
commit 0a0717a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -281,7 +281,7 @@ nr_def simple_tuple<>() -> Field {
   t.2 : Field
 }
 
-example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote _ .field) => v = 3) := by
+example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 3) := by
   simp only [simple_tuple]
   steps
   aesop