Safe Haskell	None

MAlonzo.Code.Mint.Completeness.LogRel

Documentation

d_RelExp_16 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_RelExp_16 Source #

Constructors

C_RelExp'46'constructor_159 T_D_10 T_D_10 T_'10214'_'10215'_'8600'__12 T_'10214'_'10215'_'8600'__12 AgdaAny

d_'10214't'10215'_38 :: T_RelExp_16 -> T_D_10 Source #

d_'10214't'8242''10215'_40 :: T_RelExp_16 -> T_D_10 Source #

d_'8600''10214't'10215'_42 :: T_RelExp_16 -> T_'10214'_'10215'_'8600'__12 Source #

d_'8600''10214't'8242''10215'_44 :: T_RelExp_16 -> T_'10214'_'10215'_'8600'__12 Source #

d_t'8776't'8242'_46 :: T_RelExp_16 -> AgdaAny Source #

d__'8872'_'8776'_'8758'__48 :: T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> T_Exp_70 -> () Source #

d__'8872'_'8758'__82 :: T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> () Source #

d_RelSubsts_100 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_RelSubsts_100 Source #

Constructors

C_RelSubsts'46'constructor_1871 (Integer -> T_Σ_14) (Integer -> T_Σ_14) T_'10214'_'10215's_'8600'__14 T_'10214'_'10215's_'8600'__14 AgdaAny

d_'10214'σ'10215'_122 :: T_RelSubsts_100 -> Integer -> T_Σ_14 Source #

d_'10214'δ'10215'_124 :: T_RelSubsts_100 -> Integer -> T_Σ_14 Source #

d_'8600''10214'σ'10215'_126 :: T_RelSubsts_100 -> T_'10214'_'10215's_'8600'__14 Source #

d_'8600''10214'δ'10215'_128 :: T_RelSubsts_100 -> T_'10214'_'10215's_'8600'__14 Source #

d_σ'8776'δ_130 :: T_RelSubsts_100 -> AgdaAny Source #

d__'8872's_'8776'_'8758'__132 :: T_List'8314'_24 -> T_Substs_72 -> T_Substs_72 -> T_List'8314'_24 -> () Source #

d__'8872's_'8758'__152 :: T_List'8314'_24 -> T_Substs_72 -> T_List'8314'_24 -> () Source #

d_RelExp'8658'RepTyp_162 :: T_Exp_70 -> (Integer -> T_Σ_14) -> T_Exp_70 -> (Integer -> T_Σ_14) -> Integer -> T_RelExp_16 -> T_RelTyp_314 Source #

du_RelExp'8658'RepTyp_162 :: T_RelExp_16 -> T_RelTyp_314 Source #

d_t'8776't'8242'_172 :: T_RelExp_16 -> T_𝕌_188 Source #

d_'8600''10214't'8242''10215'_174 :: T_RelExp_16 -> T_'10214'_'10215'_'8600'__12 Source #

d_'8600''10214't'10215'_176 :: T_RelExp_16 -> T_'10214'_'10215'_'8600'__12 Source #

d_'10214't'8242''10215'_178 :: T_RelExp_16 -> T_D_10 Source #

d_'10214't'10215'_180 :: T_RelExp_16 -> T_D_10 Source #