diff options
author | Son Ho | 2023-10-13 00:40:37 +0200 |
---|---|---|
committer | Son Ho | 2023-10-13 00:40:37 +0200 |
commit | 0f0e4be7dc746e2676db33f850bbeddf239eaec8 (patch) | |
tree | ea8ab9462d73f493bafeed5b914cb05514eddaa2 /backends/lean/Base/Primitives | |
parent | af78286d801b26bf7a70b8815619591d48245cb8 (diff) |
Add sup
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Primitives/Array.lean | 9 |
1 files changed, 9 insertions, 0 deletions
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. |