| 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 #
d_translation'63'_100 ∷ () → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_32) → T__'8866'_14 → T__'8866'_14 → T_Dec_32 Source #
du_translation'63'_100 ∷ () → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_32) → T__'8866'_14 → T__'8866'_14 → T_Dec_32 Source #
d_decPointwiseTranslation'63'_112 ∷ () → T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_32) → [T__'8866'_14] → [T__'8866'_14] → T_Dec_32 Source #
du_decPointwiseTranslation'63'_112 ∷ T_DecEq_6 → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → T_Dec_32) → [T__'8866'_14] → [T__'8866'_14] → T_Dec_32 Source #
d_convert'45'pointwise_1652 ∷ () → (() → 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_1652 ∷ () → [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_1676 ∷ () → (() → 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_1676 ∷ () → 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_1744 ∷ (() → 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_1744 ∷ (() → T_DecEq_6 → T__'8866'_14 → T_Translation_16) → () → T_DecEq_6 → [T__'8866'_14] → T_Pointwise_48 Source #
d_reflexive_1756 ∷ () → (() → T_DecEq_6 → T__'8866'_14 → T__'8866'_14 → ()) → T__'8866'_14 → T_DecEq_6 → T_Translation_16 Source #