{-# 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.Base 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.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.Empty
d__'8804''7495'__10 :: Integer -> Integer -> Bool
d__'8804''7495'__10 :: Integer -> Integer -> Bool
d__'8804''7495'__10 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Bool
forall a b. a -> b
coe ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d__'8804'__18 :: p -> p -> ()
d__'8804'__18 p
a0 p
a1 = ()
data T__'8804'__18 = C_z'8804'n_22 | C_s'8804's_30 T__'8804'__18
d__'60'__32 :: Integer -> Integer -> ()
d__'60'__32 :: Integer -> Integer -> ()
d__'60'__32 = Integer -> Integer -> ()
forall a. a
erased
d__'8805'__38 :: Integer -> Integer -> ()
d__'8805'__38 :: Integer -> Integer -> ()
d__'8805'__38 = Integer -> Integer -> ()
forall a. a
erased
d__'62'__44 :: Integer -> Integer -> ()
d__'62'__44 :: Integer -> Integer -> ()
d__'62'__44 = Integer -> Integer -> ()
forall a. a
erased
d__'8816'__50 :: Integer -> Integer -> ()
d__'8816'__50 :: Integer -> Integer -> ()
d__'8816'__50 = Integer -> Integer -> ()
forall a. a
erased
d__'8814'__56 :: Integer -> Integer -> ()
d__'8814'__56 :: Integer -> Integer -> ()
d__'8814'__56 = Integer -> Integer -> ()
forall a. a
erased
d__'8817'__62 :: Integer -> Integer -> ()
d__'8817'__62 :: Integer -> Integer -> ()
d__'8817'__62 = Integer -> Integer -> ()
forall a. a
erased
d__'8815'__68 :: Integer -> Integer -> ()
d__'8815'__68 :: Integer -> Integer -> ()
d__'8815'__68 = Integer -> Integer -> ()
forall a. a
erased
d_NonZero_74 :: Integer -> ()
d_NonZero_74 :: Integer -> ()
d_NonZero_74 = Integer -> ()
forall a. a
erased
d_'8802''45'nonZero_80 ::
Integer ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny
d_'8802''45'nonZero_80 :: Integer -> (T__'8801'__12 -> T_'8869'_4) -> Any
d_'8802''45'nonZero_80 Integer
v0 T__'8801'__12 -> T_'8869'_4
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> (T__'8801'__12 -> T_'8869'_4) -> Any -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_'8869'_4
v1 Any
forall a. a
erased
Integer
_ -> () -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
d_'62''45'nonZero_90 :: Integer -> T__'8804'__18 -> AgdaAny
d_'62''45'nonZero_90 :: Integer -> T__'8804'__18 -> Any
d_'62''45'nonZero_90 ~Integer
v0 T__'8804'__18
v1 = T__'8804'__18 -> Any
du_'62''45'nonZero_90 T__'8804'__18
v1
du_'62''45'nonZero_90 :: T__'8804'__18 -> AgdaAny
du_'62''45'nonZero_90 :: T__'8804'__18 -> Any
du_'62''45'nonZero_90 T__'8804'__18
v0
= (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v0) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
d_pred_94 :: Integer -> Integer
d_pred_94 :: Integer -> Integer
d_pred_94 Integer
v0
= (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 (Integer
1 :: Integer)
d__'43''8910'__98 :: Integer -> Integer -> Integer
d__'43''8910'__98 :: Integer -> Integer -> Integer
d__'43''8910'__98 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43''8910'__98 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
d__'8852'__106 :: Integer -> Integer -> Integer
d__'8852'__106 :: Integer -> Integer -> Integer
d__'8852'__106 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v0
Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'8852'__106 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
d__'8851'__116 :: Integer -> Integer -> Integer
d__'8851'__116 :: Integer -> Integer -> Integer
d__'8851'__116 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)
Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'8851'__116 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
d_'8970'_'47'2'8971'_126 :: Integer -> Integer
d_'8970'_'47'2'8971'_126 :: Integer -> Integer
d_'8970'_'47'2'8971'_126 Integer
v0
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
Integer
1 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'8970'_'47'2'8971'_126 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
d_'8968'_'47'2'8969'_130 :: Integer -> Integer
d_'8968'_'47'2'8969'_130 :: Integer -> Integer
d_'8968'_'47'2'8969'_130 Integer
v0
= (Integer -> Integer) -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer
d_'8970'_'47'2'8971'_126 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
d__'94'__134 :: Integer -> Integer -> Integer
d__'94'__134 :: Integer -> Integer -> Integer
d__'94'__134 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'94'__134 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
d_'8739'_'45'_'8739'_142 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_142 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_142 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v0
Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_142 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
d__'8804''8242'__154 :: p -> p -> ()
d__'8804''8242'__154 p
a0 p
a1 = ()
data T__'8804''8242'__154
= C_'8804''8242''45'refl_158 |
C_'8804''8242''45'step_164 T__'8804''8242'__154
d__'60''8242'__166 :: Integer -> Integer -> ()
d__'60''8242'__166 :: Integer -> Integer -> ()
d__'60''8242'__166 = Integer -> Integer -> ()
forall a. a
erased
d__'8805''8242'__172 :: Integer -> Integer -> ()
d__'8805''8242'__172 :: Integer -> Integer -> ()
d__'8805''8242'__172 = Integer -> Integer -> ()
forall a. a
erased
d__'62''8242'__178 :: Integer -> Integer -> ()
d__'62''8242'__178 :: Integer -> Integer -> ()
d__'62''8242'__178 = Integer -> Integer -> ()
forall a. a
erased
d__'8804''8243'__188 :: p -> p -> ()
d__'8804''8243'__188 p
a0 p
a1 = ()
newtype T__'8804''8243'__188
= C_less'45'than'45'or'45'equal_202 Integer
d_k_198 :: T__'8804''8243'__188 -> Integer
d_k_198 :: T__'8804''8243'__188 -> Integer
d_k_198 T__'8804''8243'__188
v0
= case T__'8804''8243'__188 -> T__'8804''8243'__188
forall a b. a -> b
coe T__'8804''8243'__188
v0 of
C_less'45'than'45'or'45'equal_202 Integer
v1 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
T__'8804''8243'__188
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_proof_200 ::
T__'8804''8243'__188 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_proof_200 :: T__'8804''8243'__188 -> T__'8801'__12
d_proof_200 = T__'8804''8243'__188 -> T__'8801'__12
forall a. a
erased
d__'60''8243'__204 :: Integer -> Integer -> ()
d__'60''8243'__204 :: Integer -> Integer -> ()
d__'60''8243'__204 = Integer -> Integer -> ()
forall a. a
erased
d__'8805''8243'__210 :: Integer -> Integer -> ()
d__'8805''8243'__210 :: Integer -> Integer -> ()
d__'8805''8243'__210 = Integer -> Integer -> ()
forall a. a
erased
d__'62''8243'__216 :: Integer -> Integer -> ()
d__'62''8243'__216 :: Integer -> Integer -> ()
d__'62''8243'__216 = Integer -> Integer -> ()
forall a. a
erased
d__'8804''8244'__222 :: p -> p -> ()
d__'8804''8244'__222 p
a0 p
a1 = ()
data T__'8804''8244'__222
= C_'8804''8244''45'refl_226 |
C_'8804''8244''45'step_232 T__'8804''8244'__222
d__'60''8244'__234 :: Integer -> Integer -> ()
d__'60''8244'__234 :: Integer -> Integer -> ()
d__'60''8244'__234 = Integer -> Integer -> ()
forall a. a
erased
d__'8805''8244'__240 :: Integer -> Integer -> ()
d__'8805''8244'__240 :: Integer -> Integer -> ()
d__'8805''8244'__240 = Integer -> Integer -> ()
forall a. a
erased
d__'62''8244'__246 :: Integer -> Integer -> ()
d__'62''8244'__246 :: Integer -> Integer -> ()
d__'62''8244'__246 = Integer -> Integer -> ()
forall a. a
erased
d_Ordering_252 :: p -> p -> ()
d_Ordering_252 p
a0 p
a1 = ()
data T_Ordering_252
= C_less_258 Integer | C_equal_262 | C_greater_268 Integer
d_compare_274 :: Integer -> Integer -> T_Ordering_252
d_compare_274 :: Integer -> Integer -> T_Ordering_252
d_compare_274 Integer
v0 Integer
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> T_Ordering_252 -> T_Ordering_252
forall a b. a -> b
coe T_Ordering_252
C_equal_262
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T_Ordering_252
forall a b. a -> b
coe ((Integer -> T_Ordering_252) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_252
C_less_258 Integer
v2)
Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> T_Ordering_252
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (Integer -> T_Ordering_252) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_252
C_greater_268 Integer
v2
Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe ((Integer -> Integer -> T_Ordering_252) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Ordering_252
d_compare_274 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))