From 17d89cc8620ab97238c7e33ebeb17368a68f9697 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Wed, 10 Jul 2024 13:26:48 +0200
Subject: [PATCH] add felt252 to types able to form constants

---
 Aegis/Types.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Aegis/Types.lean b/Aegis/Types.lean
index cab3106..3cc293b 100644
--- a/Aegis/Types.lean
+++ b/Aegis/Types.lean
@@ -147,7 +147,7 @@ partial def translate (raw : HashMap Identifier Identifier) (ctx : List Identifi
         let x ← idents.mapM <| translate raw (i :: ident :: ctx)  -- really add `ident`?
         let (lvs, tys) := x.unzip
         .ok (lvs.join, .ConstStruct ty tys)
-      | .U8 | .U16 | .U32 | .U64 | .U128 =>
+      | .U8 | .U16 | .U32 | .U64 | .U128 | .Felt252 =>
         let num : ℤ ← match ps with
         | [.const n] => pure n
         | _ => throw "parameter to numerical constant type must be a numeral"