Fix signature of core BuiltinAnomaDecode

anoma · May 15, 2024 · 049bb4a · 049bb4a
1 parent 2591c52
commit 049bb4a
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -705,10 +705,12 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               mkSmallUniv
               (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaEncode [mkVar' 0]))
           )
-      Internal.BuiltinAnomaDecode ->
+      Internal.BuiltinAnomaDecode -> do
+        natName <- getNatName
+        natSym <- getNatSymbol
         registerAxiomDef
           ( mkLambda'
-              mkSmallUniv
+              (mkTypeConstr (setInfoName natName mempty) natSym [])
               (mkLambda' (mkVar' 0) (mkBuiltinApp' OpAnomaDecode [mkVar' 0]))
           )
       Internal.BuiltinPoseidon -> do