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

MAlonzo.Code.VerifiedCompilation.UntypedTranslation

Documentation

d_Relation_4 :: () #

d_Translation_12 :: p -> p -> p -> p -> () #

data T_Translation_12 #

Constructors

C_istranslation_92 AgdaAny 
C_match_98 T_TransMatch_18 

d_TransMatch_18 :: p -> p -> p -> p -> () #

data T_TransMatch_18 #

Constructors

C_var_26 
C_ƛ_32 T_Translation_12 
C_app_42 T_Translation_12 T_Translation_12 
C_force_48 T_Translation_12 
C_delay_54 T_Translation_12 
C_con_58 
C_constr_66 T_Pointwise_48 
C_case_76 T_Pointwise_48 T_Translation_12 
C_builtin_80 
C_error_82 

d_untypedIx_102 :: Integer -> T__'8866'_14 -> Integer #

du_untypedIx_102 :: T__'8866'_14 -> Integer #

d_matchIx_136 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> Integer -> T__'8866'_14 -> T__'8866'_14 -> T_TransMatch_18 -> T__'8801'__12 #

d_translation'63'_164 :: Integer -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> T_SimplifierTag_4 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38) -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38 #

du_translation'63'_164 :: Integer -> T_SimplifierTag_4 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38) -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38 #

d_decPointwiseTranslation'63'_176 :: Integer -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> T_SimplifierTag_4 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38) -> [T__'8866'_14] -> [T__'8866'_14] -> T_ProofOrCE_38 #

du_decPointwiseTranslation'63'_176 :: Integer -> T_SimplifierTag_4 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38) -> [T__'8866'_14] -> [T__'8866'_14] -> T_ProofOrCE_38 #

d_convert'45'pointwise_1506 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> Integer -> [T__'8866'_14] -> [T__'8866'_14] -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny) -> T_Pointwise_48 -> T_Pointwise_48 #

du_convert'45'pointwise_1506 :: Integer -> [T__'8866'_14] -> [T__'8866'_14] -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny) -> T_Pointwise_48 -> T_Pointwise_48 #

d_convert_1526 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> Integer -> T__'8866'_14 -> T__'8866'_14 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny) -> T_Translation_12 -> T_Translation_12 #

du_convert_1526 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny -> AgdaAny) -> T_Translation_12 -> T_Translation_12 #

d_pointwise'45'reflexive_1590 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> (Integer -> T__'8866'_14 -> T_Translation_12) -> Integer -> [T__'8866'_14] -> T_Pointwise_48 #

du_pointwise'45'reflexive_1590 :: (Integer -> T__'8866'_14 -> T_Translation_12) -> Integer -> [T__'8866'_14] -> T_Pointwise_48 #

d_reflexive_1600 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ()) -> Integer -> T__'8866'_14 -> T_Translation_12 #

du_reflexive_1600 :: Integer -> T__'8866'_14 -> T_Translation_12 #