| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.VerifiedCompilation.UntypedTranslation
Documentation
d_Translation_8 ∷ p → p → p → p → () Source #
data T_Translation_8 Source #
Constructors
| C_istranslation_88 AgdaAny | |
| C_match_94 T_TransMatch_14 |
d_TransMatch_14 ∷ p → p → p → p → () Source #
data T_TransMatch_14 Source #
d_matchIx_132 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → Integer → T__'8866'_14 → T__'8866'_14 → T_TransMatch_14 → T__'8801'__12 Source #
d_translation'63'_160 ∷ Integer → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_38) → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_38 Source #
du_translation'63'_160 ∷ Integer → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_38) → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_38 Source #
d_decPointwiseTranslation'63'_172 ∷ Integer → (Integer → T__'8866'_14 → T__'8866'_14 → ()) → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_38) → [T__'8866'_14] → [T__'8866'_14] → T_ProofOrCE_38 Source #
du_decPointwiseTranslation'63'_172 ∷ Integer → T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_10 → (Integer → T__'8866'_14 → T__'8866'_14 → T_ProofOrCE_38) → [T__'8866'_14] → [T__'8866'_14] → T_ProofOrCE_38 Source #
d_convert'45'pointwise_1502 ∷ (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_1502 ∷ 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_1522 ∷ (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_8 → T_Translation_8 Source #
du_convert_1522 ∷ Integer → T__'8866'_14 → T__'8866'_14 → (Integer → T__'8866'_14 → T__'8866'_14 → AgdaAny → AgdaAny) → T_Translation_8 → T_Translation_8 Source #
d_pointwise'45'reflexive_1586 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → (Integer → T__'8866'_14 → T_Translation_8) → Integer → [T__'8866'_14] → T_Pointwise_48 Source #
du_pointwise'45'reflexive_1586 ∷ (Integer → T__'8866'_14 → T_Translation_8) → Integer → [T__'8866'_14] → T_Pointwise_48 Source #
d_reflexive_1596 ∷ (Integer → T__'8866'_14 → T__'8866'_14 → ()) → Integer → T__'8866'_14 → T_Translation_8 Source #