Safe Haskell	None

MAlonzo.Code.Mint.Semantics.PER

Documentation

d_Ty_6 :: () Source #

d_Evs_8 :: () Source #

d_Bot_10 :: T_Dn_12 -> T_Dn_12 -> () Source #

d_Top_22 :: T_Df_14 -> T_Df_14 -> () Source #

d_TopT_34 :: T_D_10 -> T_D_10 -> () Source #

d_Nat_46 :: p1 -> p2 -> () Source #

data T_Nat_46 Source #

Constructors

C_ze_48
C_su_50 T_Nat_46
C_ne_52 (T_List'8314'_24 -> (Integer -> Integer) -> T_Σ_14)

d_Neu_54 :: p1 -> p2 -> () Source #

newtype T_Neu_54 Source #

Constructors

C_ne_56 (T_List'8314'_24 -> (Integer -> Integer) -> T_Σ_14)

d_ΠRT_68 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_ΠRT_68 Source #

Constructors

C_ΠRT'46'constructor_1945 T_D_10 T_D_10 T_'10214'_'10215'_'8600'__12 T_'10214'_'10215'_'8600'__12 AgdaAny

d_'10214'T'10215'_90 :: T_ΠRT_68 -> T_D_10 Source #

d_'10214'T'8242''10215'_92 :: T_ΠRT_68 -> T_D_10 Source #

d_'8600''10214'T'10215'_94 :: T_ΠRT_68 -> T_'10214'_'10215'_'8600'__12 Source #

d_'8600''10214'T'8242''10215'_96 :: T_ΠRT_68 -> T_'10214'_'10215'_'8600'__12 Source #

d_T'8776'T'8242'_98 :: T_ΠRT_68 -> AgdaAny Source #

d_'9633''770'_108 :: p1 -> p2 -> p3 -> p4 -> () Source #

data T_'9633''770'_108 Source #

Constructors

C_'9633''770''46'constructor_2379 T_D_10 T_D_10 T_unbox'8729'_'44'_'8600'__8 T_unbox'8729'_'44'_'8600'__8 AgdaAny

d_ua_128 :: T_'9633''770'_108 -> T_D_10 Source #

d_ub_130 :: T_'9633''770'_108 -> T_D_10 Source #

d_'8600'ua_132 :: T_'9633''770'_108 -> T_unbox'8729'_'44'_'8600'__8 Source #

d_'8600'ub_134 :: T_'9633''770'_108 -> T_unbox'8729'_'44'_'8600'__8 Source #

d_ua'8776'ub_136 :: T_'9633''770'_108 -> AgdaAny Source #

d_Π'770'_148 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_Π'770'_148 Source #

Constructors

C_Π'770''46'constructor_2789 T_D_10 T_D_10 T__'8729'_'8600'__6 T__'8729'_'8600'__6 AgdaAny

d_fa_170 :: T_Π'770'_148 -> T_D_10 Source #

d_fa'8242'_172 :: T_Π'770'_148 -> T_D_10 Source #

d_'8600'fa_174 :: T_Π'770'_148 -> T__'8729'_'8600'__6 Source #

d_'8600'fa'8242'_176 :: T_Π'770'_148 -> T__'8729'_'8600'__6 Source #

d_fa'8776'fa'8242'_178 :: T_Π'770'_148 -> AgdaAny Source #

d_𝕌_188 :: p1 -> p2 -> p3 -> p4 -> () Source #

data T_𝕌_188 Source #

Constructors

C_ne_192 (T_List'8314'_24 -> (Integer -> Integer) -> T_Σ_14)
C_N_194
C_U_200 T__'8804'__18
C_'9633'_204 ((Integer -> Integer) -> T_𝕌_188)
C_Π_216 ((Integer -> Integer) -> T_𝕌_188) (T_D_10 -> T_D_10 -> (Integer -> Integer) -> AgdaAny -> T_ΠRT_68)

d_El_190 :: Integer -> (Integer -> T__'8804'__18 -> T_D_10 -> T_D_10 -> ()) -> T_D_10 -> T_D_10 -> T_𝕌_188 -> T_D_10 -> T_D_10 -> () Source #

d_𝕌'45'wellfounded_254 :: Integer -> Integer -> T__'8804'__18 -> T_D_10 -> T_D_10 -> () Source #

d_𝕌_278 :: p1 -> p2 -> p3 -> () Source #

d_𝕌_296 :: Integer -> T_D_10 -> T_D_10 -> () Source #

d_El_300 :: T_D_10 -> T_D_10 -> Integer -> T_𝕌_188 -> T_D_10 -> T_D_10 -> () Source #

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

data T_RelTyp_314 Source #

Constructors

C_RelTyp'46'constructor_12303 T_D_10 T_D_10 T_'10214'_'10215'_'8600'__12 T_'10214'_'10215'_'8600'__12 T_𝕌_188

d_'10214'T'10215'_336 :: T_RelTyp_314 -> T_D_10 Source #

d_'10214'T'8242''10215'_338 :: T_RelTyp_314 -> T_D_10 Source #

d_'8600''10214'T'10215'_340 :: T_RelTyp_314 -> T_'10214'_'10215'_'8600'__12 Source #

d_'8600''10214'T'8242''10215'_342 :: T_RelTyp_314 -> T_'10214'_'10215'_'8600'__12 Source #

d_T'8776'T'8242'_344 :: T_RelTyp_314 -> T_𝕌_188 Source #

d_'8872'_'8776'__346 :: p1 -> p2 -> () Source #

data T_'8872'_'8776'__346 Source #

Constructors

C_'91''93''45''8776'_350
C_κ'45'cong_352 T_List'8314'_24 T_List'8314'_24 T_'8872'_'8776'__346
C_'8762''45'cong_362 T_List'8314'_24 T_List'8314'_24 T_Exp_70 T_Exp_70 Integer T_'8872'_'8776'__346 ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314)

d_'10214'_'10215'ρ_348 :: T_List'8314'_24 -> T_List'8314'_24 -> T_'8872'_'8776'__346 -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> () Source #

d_T'8776'T'8242'_386 :: T_List'8314'_24 -> T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> Integer -> T_'8872'_'8776'__346 -> ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_𝕌_188 Source #

du_T'8776'T'8242'_386 :: ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_𝕌_188 Source #

d_'8600''10214'T'8242''10215'_388 :: T_List'8314'_24 -> T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> Integer -> T_'8872'_'8776'__346 -> ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_'10214'_'10215'_'8600'__12 Source #

du_'8600''10214'T'8242''10215'_388 :: ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_'10214'_'10215'_'8600'__12 Source #

d_'8600''10214'T'10215'_390 :: T_List'8314'_24 -> T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> Integer -> T_'8872'_'8776'__346 -> ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_'10214'_'10215'_'8600'__12 Source #

du_'8600''10214'T'10215'_390 :: ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_'10214'_'10215'_'8600'__12 Source #

d_'10214'T'8242''10215'_392 :: T_List'8314'_24 -> T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> Integer -> T_'8872'_'8776'__346 -> ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_D_10 Source #

du_'10214'T'8242''10215'_392 :: ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_D_10 Source #

d_'10214'T'10215'_394 :: T_List'8314'_24 -> T_List'8314'_24 -> T_Exp_70 -> T_Exp_70 -> Integer -> T_'8872'_'8776'__346 -> ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_D_10 Source #

du_'10214'T'10215'_394 :: ((Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_RelTyp_314) -> (Integer -> T_Σ_14) -> (Integer -> T_Σ_14) -> AgdaAny -> T_D_10 Source #

d_'8872'__396 :: T_List'8314'_24 -> () Source #