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/coq/Primitives.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backends/coq')

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 8d6c9c8d..b92eb967 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -433,6 +433,9 @@ Qed.
 (* TODO: finish the definitions *)
 Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n.
 
+(* For initialization *)
+Axiom array_repeat : forall {T : Type} (n : usize) (x : T), array T n.
+
 Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
 Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
 Axiom array_index_mut_back : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n).
-- 
cgit v1.2.3