| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation.UntypedTranslation
Documentation
d_Relation_4 ∷ () Source #
d_Translation_16 ∷ p → p → p → p → p → () Source #
data T_Translation_16 Source #
Constructors
| C_istranslation_100 AgdaAny | |
| C_match_106 T_TransMatch_24 |
d_TransMatch_24 ∷ p → p → p → p → p → () Source #
data T_TransMatch_24 Source #
d_untypedIx_110 ∷ () → T__'8866'_14 → Integer Source #
d_matchIx_146 ∷ (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → () → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_TransMatch_24 → T__'8801'__12 Source #
d_translation'63'_174 ∷ () → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_20) → T__'8866'_14 → T__'8866'_14 → T_Dec_20 Source #
du_translation'63'_174 ∷ () → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_20) → T__'8866'_14 → T__'8866'_14 → T_Dec_20 Source #
d_decPointwiseTranslation'63'_186 ∷ () → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_20) → [T__'8866'_14] → [T__'8866'_14] → T_Dec_20 Source #
du_decPointwiseTranslation'63'_186 ∷ T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_20) → [T__'8866'_14] → [T__'8866'_14] → T_Dec_20 Source #
d_convert'45'pointwise_1024 ∷ () → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → [T__'8866'_14] → [T__'8866'_14] → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → T_Pointwise_48 → T_Pointwise_48 Source #
du_convert'45'pointwise_1024 ∷ () → [T__'8866'_14] → [T__'8866'_14] → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → T_Pointwise_48 → T_Pointwise_48 Source #
d_convert_1048 ∷ () → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → T__'8866'_14 → T__'8866'_14 → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → T_Translation_16 → T_Translation_16 Source #
du_convert_1048 ∷ () → T__'8866'_14 → T__'8866'_14 → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → T_Translation_16 → T_Translation_16 Source #
d_pointwise'45'reflexive_1116 ∷ (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T_Translation_16) → () → T_DecEq_6 → [T__'8866'_14] → T_Pointwise_48 Source #
du_pointwise'45'reflexive_1116 ∷ (() → T_DecEq_6 → T__'8866'_14 → T_Translation_16) → () → T_DecEq_6 → [T__'8866'_14] → T_Pointwise_48 Source #
d_reflexive_1128 ∷ () → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → T__'8866'_14 → T_DecEq_6 → T_Translation_16 Source #