Fix signature of core BuiltinAnomaDecode

anoma · May 14, 2024 · 83720ff · 83720ff
1 parent f932a21
commit 83720ff
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
@@ -708,10 +708,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