From 0f0e4be7dc746e2676db33f850bbeddf239eaec8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 13 Oct 2023 00:40:37 +0200
Subject: Add sup

---
 backends/lean/Base/Primitives/Array.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
index 6c95fd78..49c84bee 100644
--- a/backends/lean/Base/Primitives/Array.lean
+++ b/backends/lean/Base/Primitives/Array.lean
@@ -51,6 +51,15 @@ def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Re
   | none => fail .arrayOutOfBounds
   | some x => ret x
 
+-- For initialization
+def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
+  ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩
+
+@[pspec]
+theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
+  ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by
+  simp [Array.repeat]
+
 /- In the theorems below: we don't always need the `∃ ..`, but we use one
    so that `progress` introduces an opaque variable and an equality. This
    helps control the context.
-- 
cgit v1.2.3