{-# 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.Induction where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Primitive

-- Induction.RecStruct
d_RecStruct_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> ()
d_RecStruct_20 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
d_RecStruct_20 = T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Induction.RecursorBuilder
d_RecursorBuilder_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  ((AgdaAny -> ()) -> AgdaAny -> ()) -> ()
d_RecursorBuilder_24 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
d_RecursorBuilder_24 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Induction.Recursor
d_Recursor_30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  ((AgdaAny -> ()) -> AgdaAny -> ()) -> ()
d_Recursor_30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
d_Recursor_30 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Induction.build
d_build_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  ((AgdaAny -> ()) -> AgdaAny -> ()) ->
  ((AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_build_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_build_36 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~(AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18
v4 (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v5 AgdaAny -> T_Level_18
v6 AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8
  = ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_build_36 (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v5 AgdaAny -> T_Level_18
v6 AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8
du_build_36 ::
  ((AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_build_36 :: ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_build_36 (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v0 AgdaAny -> T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 (((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v0 AgdaAny -> T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3)
-- Induction.SubsetRecursorBuilder
d_SubsetRecursorBuilder_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> ()
d_SubsetRecursorBuilder_46 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
d_SubsetRecursorBuilder_46 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Induction.SubsetRecursor
d_SubsetRecursor_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> ((AgdaAny -> ()) -> AgdaAny -> ()) -> ()
d_SubsetRecursor_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
d_SubsetRecursor_54 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
-- Induction.subsetBuild
d_subsetBuild_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  ((AgdaAny -> ()) -> AgdaAny -> ()) ->
  ((AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny -> AgdaAny) ->
   AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_subsetBuild_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> (AgdaAny -> AgdaAny -> AgdaAny)
    -> AgdaAny
    -> AgdaAny
    -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_subsetBuild_62 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~(AgdaAny -> T_Level_18) -> AgdaAny -> T_Level_18
v6 (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subsetBuild_62 (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> T_Level_18
v8 AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_subsetBuild_62 ::
  ((AgdaAny -> ()) ->
   (AgdaAny -> AgdaAny -> AgdaAny) ->
   AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_subsetBuild_62 :: ((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subsetBuild_62 (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 (((AgdaAny -> T_Level_18)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> T_Level_18
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)