{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Relation.Binary.HeterogeneousEquality.Core where
import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
word64ToNat)
import MAlonzo.RTE qualified
d__'8773'__22 :: p -> p -> p -> p -> p -> p -> ()
d__'8773'__22 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T__'8773'__22 = C_refl_28
d_'8773''45'to'45''8801'_34 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
T__'8773'__22 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8773''45'to'45''8801'_34 :: () -> () -> AgdaAny -> AgdaAny -> T__'8773'__22 -> T__'8801'__12
d_'8773''45'to'45''8801'_34 = () -> () -> AgdaAny -> AgdaAny -> T__'8773'__22 -> T__'8801'__12
forall a. a
erased
d_'8801''45'to'45''8773'_40 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> T__'8773'__22
d_'8801''45'to'45''8773'_40 :: () -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8773'__22
d_'8801''45'to'45''8773'_40 = () -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8773'__22
forall a. a
erased