| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation.UntypedTranslation
Documentation
d_Relation_4 ∷ () Source #
d_Translation_12 ∷ p → p → p → p → () Source #
data T_Translation_12 Source #
Constructors
| C_istranslation_92 AgdaAny | |
| C_match_98 T_TransMatch_18 |
d_TransMatch_18 ∷ p → p → p → p → () Source #
data T_TransMatch_18 Source #
d_matchIx_136 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → Integer → T__'8866'_14 → T__'8866'_14 → T_TransMatch_18 → T__'8801'__12 Source #
d_translation'63'_164 ∷ Integer → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → T_SimplifierTag_4 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_54) → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_54 Source #
du_translation'63'_164 ∷ Integer → T_SimplifierTag_4 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_54) → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_54 Source #
d_decPointwiseTranslation'63'_176 ∷ Integer → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → T_SimplifierTag_4 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_54) → [T__'8866'_14] → [T__'8866'_14] → T_ProofOrCE_54 Source #
du_decPointwiseTranslation'63'_176 ∷ Integer → T_SimplifierTag_4 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_54) → [T__'8866'_14] → [T__'8866'_14] → T_ProofOrCE_54 Source #
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 Source #
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 Source #
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 Source #
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 Source #
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 Source #
du_pointwise'45'reflexive_1590 ∷ (Integer → T__'8866'_14 → T_Translation_12) → Integer → [T__'8866'_14] → T_Pointwise_48 Source #
d_reflexive_1600 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → Integer → T__'8866'_14 → T_Translation_12 Source #