plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Induction

Documentation

d_RecursorBuilder_24 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> () #

d_Recursor_30 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> () #

d_build_36 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> ((AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

du_build_36 :: ((AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #

d_SubsetRecursorBuilder_46 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> ()) -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> () #

d_SubsetRecursor_54 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> T_Level_18 -> (AgdaAny -> ()) -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> () #

d_subsetBuild_62 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> ()) -> T_Level_18 -> T_Level_18 -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> ((AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #

du_subsetBuild_62 :: ((AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny #