{-# 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.Data.Nat.Properties.Core 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.Data.Nat.Base

-- Data.Nat.Properties.Core.≤-pred
d_'8804''45'pred_12 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
d_'8804''45'pred_12 :: Integer -> Integer -> T__'8804'__18 -> T__'8804'__18
d_'8804''45'pred_12 ~Integer
v0 ~Integer
v1 T__'8804'__18
v2 = T__'8804'__18 -> T__'8804'__18
du_'8804''45'pred_12 T__'8804'__18
v2
du_'8804''45'pred_12 ::
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__18
du_'8804''45'pred_12 :: T__'8804'__18 -> T__'8804'__18
du_'8804''45'pred_12 T__'8804'__18
v0
  = case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v0 of
      MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v3 -> T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v3
      T__'8804'__18
_ -> T__'8804'__18
forall a. a
MAlonzo.RTE.mazUnreachableError