Skip to content

Commit cc0f02f

Browse files
committed
Add examples of module parametrization malonzo
1 parent 2553b3c commit cc0f02f

1 file changed

Lines changed: 75 additions & 0 deletions

File tree

  • plutus-metatheory/src/MAlonzo/Code

plutus-metatheory/src/MAlonzo/Code/Utils.hs

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -622,3 +622,78 @@ cover_Kind_652 x
622622
Star -> ()
623623
Sharp -> ()
624624
Arrow _ _ -> ()
625+
-- Utils.M.f
626+
d_f_670 :: () -> AgdaAny -> AgdaAny
627+
d_f_670 ~v0 v1 = du_f_670 v1
628+
du_f_670 :: AgdaAny -> AgdaAny
629+
du_f_670 v0 = coe v0
630+
-- Utils.MNat.f
631+
d_f_676 :: Integer -> Integer
632+
d_f_676 v0 = coe v0
633+
-- Utils.testM
634+
d_testM_680 :: () -> AgdaAny -> AgdaAny
635+
d_testM_680 ~v0 v1 = du_testM_680 v1
636+
du_testM_680 :: AgdaAny -> AgdaAny
637+
du_testM_680 v0 = coe v0
638+
-- Utils.ByteString'
639+
d_ByteString''_682 = ()
640+
data T_ByteString''_682
641+
= C_mkBS_708 AgdaAny (AgdaAny -> AgdaAny -> AgdaAny)
642+
(T_List_384 AgdaAny -> AgdaAny) (AgdaAny -> T_List_384 AgdaAny)
643+
-- Utils.ByteString'.W8
644+
d_W8_696 :: T_ByteString''_682 -> ()
645+
d_W8_696 = erased
646+
-- Utils.ByteString'.BS
647+
d_BS_698 :: T_ByteString''_682 -> ()
648+
d_BS_698 = erased
649+
-- Utils.ByteString'.empty
650+
d_empty_700 :: T_ByteString''_682 -> AgdaAny
651+
d_empty_700 v0
652+
= case coe v0 of
653+
C_mkBS_708 v3 v4 v5 v6 -> coe v3
654+
_ -> MAlonzo.RTE.mazUnreachableError
655+
-- Utils.ByteString'.cons
656+
d_cons_702 :: T_ByteString''_682 -> AgdaAny -> AgdaAny -> AgdaAny
657+
d_cons_702 v0
658+
= case coe v0 of
659+
C_mkBS_708 v3 v4 v5 v6 -> coe v4
660+
_ -> MAlonzo.RTE.mazUnreachableError
661+
-- Utils.ByteString'.pack
662+
d_pack_704 :: T_ByteString''_682 -> T_List_384 AgdaAny -> AgdaAny
663+
d_pack_704 v0
664+
= case coe v0 of
665+
C_mkBS_708 v3 v4 v5 v6 -> coe v5
666+
_ -> MAlonzo.RTE.mazUnreachableError
667+
-- Utils.ByteString'.unpack
668+
d_unpack_706 :: T_ByteString''_682 -> AgdaAny -> T_List_384 AgdaAny
669+
d_unpack_706 v0
670+
= case coe v0 of
671+
C_mkBS_708 v3 v4 v5 v6 -> coe v6
672+
_ -> MAlonzo.RTE.mazUnreachableError
673+
-- Utils.b
674+
d_b_710 :: T_ByteString''_682
675+
d_b_710
676+
= coe
677+
C_mkBS_708 (coe C_'91''93'_388) (coe C__'8759'__390) (\ v0 -> v0)
678+
(\ v0 -> v0)
679+
-- Utils.AST1._.BS
680+
d_BS_722 :: T_ByteString''_682 -> ()
681+
d_BS_722 = erased
682+
-- Utils.AST1._.W8
683+
d_W8_724 :: T_ByteString''_682 -> ()
684+
d_W8_724 = erased
685+
-- Utils.AST1._.cons
686+
d_cons_726 :: T_ByteString''_682 -> AgdaAny -> AgdaAny -> AgdaAny
687+
d_cons_726 v0 = coe d_cons_702 (coe v0)
688+
-- Utils.AST1._.empty
689+
d_empty_728 :: T_ByteString''_682 -> AgdaAny
690+
d_empty_728 v0 = coe d_empty_700 (coe v0)
691+
-- Utils.AST1._.pack
692+
d_pack_730 :: T_ByteString''_682 -> T_List_384 AgdaAny -> AgdaAny
693+
d_pack_730 v0 = coe d_pack_704 (coe v0)
694+
-- Utils.AST1._.unpack
695+
d_unpack_732 :: T_ByteString''_682 -> AgdaAny -> T_List_384 AgdaAny
696+
d_unpack_732 v0 = coe d_unpack_706 (coe v0)
697+
-- Utils.AST1.x
698+
d_x_734 :: T_ByteString''_682 -> AgdaAny
699+
d_x_734 v0 = coe d_empty_700 (coe v0)

0 commit comments

Comments
 (0)