-module('Idris.Idris2.Core.Reflect').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--reify-9472'/11,
  'case--reify-9263'/10,
  'case--reify-8883'/13,
  'case--reify-8652'/10,
  'case--reify-8443'/10,
  'case--reify-8237'/10,
  'case--reify-7028'/11,
  'case--reify-6623'/11,
  'case--reflect-6536'/7,
  'case--reify-6072'/11,
  'case--reify-5894'/10,
  'case--reify-5642'/16,
  'case--reify-5346'/13,
  'case--reify-5096'/14,
  'case--reify-4770'/13,
  'case--reify-4529'/11,
  'case--reify-4352'/10,
  'case--getCon-3721'/5,
  'dn--un--reify_Reify__Visibility'/4,
  'dn--un--reify_Reify__TotalReq'/4,
  'dn--un--reify_Reify__String'/4,
  'dn--un--reify_Reify__RigCount'/4,
  'dn--un--reify_Reify__Nat'/4,
  'dn--un--reify_Reify__Namespace'/4,
  'dn--un--reify_Reify__NameType'/4,
  'dn--un--reify_Reify__Name'/4,
  'dn--un--reify_Reify__LazyReason'/4,
  'dn--un--reify_Reify__Integer'/4,
  'dn--un--reify_Reify__Int'/4,
  'dn--un--reify_Reify__FC'/4,
  'dn--un--reify_Reify__Double'/4,
  'dn--un--reify_Reify__Constant'/4,
  'dn--un--reify_Reify__Char'/4,
  'dn--un--reify_Reify__Bool'/4,
  'dn--un--reify_Reify__(|Unit,MkUnit|)'/5,
  'dn--un--reify_Reify__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'/7,
  'dn--un--reify_Reify__(PiInfo $t)'/6,
  'dn--un--reify_Reify__(Maybe $a)'/6,
  'dn--un--reify_Reify__(List1 $a)'/6,
  'dn--un--reify_Reify__(List $a)'/6,
  'dn--un--reflect_Reflect__Visibility'/6,
  'dn--un--reflect_Reflect__TotalReq'/6,
  'dn--un--reflect_Reflect__String'/7,
  'dn--un--reflect_Reflect__RigCount'/6,
  'dn--un--reflect_Reflect__Nat'/6,
  'dn--un--reflect_Reflect__Namespace'/7,
  'dn--un--reflect_Reflect__NameType'/6,
  'dn--un--reflect_Reflect__Name'/6,
  'dn--un--reflect_Reflect__LazyReason'/6,
  'dn--un--reflect_Reflect__Integer'/7,
  'dn--un--reflect_Reflect__Int'/7,
  'dn--un--reflect_Reflect__FC'/6,
  'dn--un--reflect_Reflect__Double'/7,
  'dn--un--reflect_Reflect__Constant'/6,
  'dn--un--reflect_Reflect__Char'/7,
  'dn--un--reflect_Reflect__Bool'/6,
  'dn--un--reflect_Reflect__(|Unit,MkUnit|)'/7,
  'dn--un--reflect_Reflect__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'/9,
  'dn--un--reflect_Reflect__(PiInfo $t)'/8,
  'dn--un--reflect_Reflect__(Maybe $a)'/8,
  'dn--un--reflect_Reflect__(List1 $a)'/8,
  'dn--un--reflect_Reflect__(List $a)'/8,
  'dn--un--__Impl_Reify_Visibility'/4,
  'dn--un--__Impl_Reify_TotalReq'/4,
  'dn--un--__Impl_Reify_String'/4,
  'dn--un--__Impl_Reify_RigCount'/4,
  'dn--un--__Impl_Reify_Nat'/4,
  'dn--un--__Impl_Reify_Namespace'/4,
  'dn--un--__Impl_Reify_NameType'/4,
  'dn--un--__Impl_Reify_Name'/4,
  'dn--un--__Impl_Reify_LazyReason'/4,
  'dn--un--__Impl_Reify_Integer'/4,
  'dn--un--__Impl_Reify_Int'/4,
  'dn--un--__Impl_Reify_FC'/4,
  'dn--un--__Impl_Reify_Double'/4,
  'dn--un--__Impl_Reify_Constant'/4,
  'dn--un--__Impl_Reify_Char'/4,
  'dn--un--__Impl_Reify_Bool'/4,
  'dn--un--__Impl_Reify_(|Unit,MkUnit|)'/5,
  'dn--un--__Impl_Reify_(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'/7,
  'dn--un--__Impl_Reify_(PiInfo $t)'/6,
  'dn--un--__Impl_Reify_(Maybe $a)'/6,
  'dn--un--__Impl_Reify_(List1 $a)'/6,
  'dn--un--__Impl_Reify_(List $a)'/6,
  'dn--un--__Impl_Reflect_Visibility'/6,
  'dn--un--__Impl_Reflect_TotalReq'/6,
  'dn--un--__Impl_Reflect_String'/7,
  'dn--un--__Impl_Reflect_RigCount'/6,
  'dn--un--__Impl_Reflect_Nat'/6,
  'dn--un--__Impl_Reflect_Namespace'/7,
  'dn--un--__Impl_Reflect_NameType'/6,
  'dn--un--__Impl_Reflect_Name'/6,
  'dn--un--__Impl_Reflect_LazyReason'/6,
  'dn--un--__Impl_Reflect_Integer'/7,
  'dn--un--__Impl_Reflect_Int'/7,
  'dn--un--__Impl_Reflect_FC'/6,
  'dn--un--__Impl_Reflect_Double'/7,
  'dn--un--__Impl_Reflect_Constant'/6,
  'dn--un--__Impl_Reflect_Char'/7,
  'dn--un--__Impl_Reflect_Bool'/6,
  'dn--un--__Impl_Reflect_(|Unit,MkUnit|)'/6,
  'dn--un--__Impl_Reflect_(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'/9,
  'dn--un--__Impl_Reflect_(PiInfo $t)'/8,
  'dn--un--__Impl_Reflect_(Maybe $a)'/8,
  'dn--un--__Impl_Reflect_(List1 $a)'/8,
  'dn--un--__Impl_Reflect_(List $a)'/8,
  'un--reify'/6,
  'un--reflectionttimp'/1,
  'un--reflectiontt'/1,
  'un--reflection'/1,
  'un--reflect'/8,
  'un--primio'/1,
  'un--preludetypes'/1,
  'un--getCon'/5,
  'un--cantReify'/5,
  'un--cantReflect'/4,
  'un--builtin'/1,
  'un--basics'/1,
  'un--appCon'/6
]).
'case--reify-9472'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V10 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V11, V12) -> case V11 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V13, V14) -> case V14 of {'Idris.Core.Name.UN', E4} -> (fun (V15) -> case V15 of <<"MkFC"/utf8>> -> case V12 of [E5 | E6] -> (fun (V16, V17) -> case V17 of [E7 | E8] -> (fun (V18, V19) -> case V19 of [E9 | E10] -> (fun (V20, V21) -> case V21 of [] -> fun (V22) -> begin (V26 = begin (V23 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V16))(V22))), case V23 of {'Idris.Prelude.Types.Left', E11} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V25) -> (('dn--un--reify_Reify__String'(V8, V0, V7, V25))(V22)) end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V26 of {'Idris.Prelude.Types.Left', E13} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V28) -> begin (V40 = begin (V29 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V18))(V22))), case V29 of {'Idris.Prelude.Types.Left', E15} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E15)); {'Idris.Prelude.Types.Right', E16} -> (fun (V31) -> (('dn--un--reify_Reify__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> ('dn--un--reify_Reify__Int'(V32, V33, V34, V35)) end end end end, fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> ('dn--un--reify_Reify__Int'(V36, V37, V38, V39)) end end end end}, V8, V0, V7, V31))(V22)) end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V40 of {'Idris.Prelude.Types.Left', E17} -> (fun (V41) -> {'Idris.Prelude.Types.Left', V41} end(E17)); {'Idris.Prelude.Types.Right', E18} -> (fun (V42) -> begin (V54 = begin (V43 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V20))(V22))), case V43 of {'Idris.Prelude.Types.Left', E19} -> (fun (V44) -> {'Idris.Prelude.Types.Left', V44} end(E19)); {'Idris.Prelude.Types.Right', E20} -> (fun (V45) -> (('dn--un--reify_Reify__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', fun (V46) -> fun (V47) -> fun (V48) -> fun (V49) -> ('dn--un--reify_Reify__Int'(V46, V47, V48, V49)) end end end end, fun (V50) -> fun (V51) -> fun (V52) -> fun (V53) -> ('dn--un--reify_Reify__Int'(V50, V51, V52, V53)) end end end end}, V8, V0, V7, V45))(V22)) end(E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V54 of {'Idris.Prelude.Types.Left', E21} -> (fun (V55) -> {'Idris.Prelude.Types.Left', V55} end(E21)); {'Idris.Prelude.Types.Right', E22} -> (fun (V56) -> {'Idris.Prelude.Types.Right', {'Idris.Core.FC.MkFC', V28, V42, V56}} end(E22)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V57) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V57)) end end end(E9, E10)); _ -> fun (V58) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V58)) end end end(E7, E8)); _ -> fun (V59) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V59)) end end end(E5, E6)); _ -> fun (V60) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V60)) end end; <<"EmptyFC"/utf8>> -> fun (V61) -> {'Idris.Prelude.Types.Right', {'Idris.Core.FC.EmptyFC'}} end; _ -> fun (V62) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V62)) end end end(E4)); _ -> fun (V63) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V63)) end end end(E2, E3)); _ -> fun (V64) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V64)) end end end(E0, E1)); _ -> fun (V65) -> ('un--cantReify'('erased', 'erased', V6, <<"FC"/utf8>>, V65)) end end.
'case--reify-9263'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.Name.UN', E2} -> (fun (V12) -> case V12 of <<"LInf"/utf8>> -> fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.LInf'}} end; <<"LLazy"/utf8>> -> fun (V14) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.LLazy'}} end; <<"LUnknown"/utf8>> -> fun (V15) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.LUnknown'}} end; _ -> fun (V16) -> ('un--cantReify'('erased', 'erased', V6, <<"LazyReason"/utf8>>, V16)) end end end(E2)); _ -> fun (V17) -> ('un--cantReify'('erased', 'erased', V6, <<"LazyReason"/utf8>>, V17)) end end end(E0, E1)); _ -> fun (V18) -> ('un--cantReify'('erased', 'erased', V6, <<"LazyReason"/utf8>>, V18)) end end.
'case--reify-8883'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V13, V14) -> case V13 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V15, V16) -> case V16 of {'Idris.Core.Name.UN', E4} -> (fun (V17) -> case V17 of <<"ImplicitArg"/utf8>> -> fun (V18) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Implicit'}} end; <<"ExplicitArg"/utf8>> -> fun (V19) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Explicit'}} end; <<"AutoImplicit"/utf8>> -> fun (V20) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.AutoImplicit'}} end; <<"DefImplicit"/utf8>> -> case V14 of [E5 | E6] -> (fun (V21, V22) -> case V22 of [E7 | E8] -> (fun (V23, V24) -> case V24 of [] -> fun (V25) -> begin (V29 = begin (V26 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V10, V2, V9, V23))(V25))), case V26 of {'Idris.Prelude.Types.Left', E9} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V28) -> (((((V1(V10))(V2))(V9))(V28))(V25)) end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V29 of {'Idris.Prelude.Types.Left', E11} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V31) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.DefImplicit', V31}} end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V32) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V32)) end end end(E7, E8)); _ -> fun (V33) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V33)) end end end(E5, E6)); _ -> fun (V34) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V34)) end end; _ -> fun (V35) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V35)) end end end(E4)); _ -> fun (V36) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V36)) end end end(E2, E3)); _ -> fun (V37) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V37)) end end end(E0, E1)); _ -> fun (V38) -> ('un--cantReify'('erased', 'erased', V8, <<"PiInfo"/utf8>>, V38)) end end.
'case--reify-8652'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.Name.UN', E2} -> (fun (V12) -> case V12 of <<"M0"/utf8>> -> fun (V13) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V14) -> fun (V15) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V14, V15)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V16) -> fun (V17) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V16, V17)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))} end; <<"M1"/utf8>> -> fun (V18) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.Semiring':'un--linear'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V19) -> fun (V20) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V19, V20)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V21) -> fun (V22) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V21, V22)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))} end; <<"MW"/utf8>> -> fun (V23) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--top_Top__ZeroOneOmega'())} end; _ -> fun (V24) -> ('un--cantReify'('erased', 'erased', V6, <<"Count"/utf8>>, V24)) end end end(E2)); _ -> fun (V25) -> ('un--cantReify'('erased', 'erased', V6, <<"Count"/utf8>>, V25)) end end end(E0, E1)); _ -> fun (V26) -> ('un--cantReify'('erased', 'erased', V6, <<"Count"/utf8>>, V26)) end end.
'case--reify-8443'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.Name.UN', E2} -> (fun (V12) -> case V12 of <<"Total"/utf8>> -> fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Total'}} end; <<"CoveringOnly"/utf8>> -> fun (V14) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.CoveringOnly'}} end; <<"PartialOK"/utf8>> -> fun (V15) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PartialOK'}} end; _ -> fun (V16) -> ('un--cantReify'('erased', 'erased', V6, <<"TotalReq"/utf8>>, V16)) end end end(E2)); _ -> fun (V17) -> ('un--cantReify'('erased', 'erased', V6, <<"TotalReq"/utf8>>, V17)) end end end(E0, E1)); _ -> fun (V18) -> ('un--cantReify'('erased', 'erased', V6, <<"TotalReq"/utf8>>, V18)) end end.
'case--reify-8237'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.Name.UN', E2} -> (fun (V12) -> case V12 of <<"Private"/utf8>> -> fun (V13) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Private'}} end; <<"Export"/utf8>> -> fun (V14) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Export'}} end; <<"Public"/utf8>> -> fun (V15) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Public'}} end; _ -> fun (V16) -> ('un--cantReify'('erased', 'erased', V6, <<"Visibility"/utf8>>, V16)) end end end(E2)); _ -> fun (V17) -> ('un--cantReify'('erased', 'erased', V6, <<"Visibility"/utf8>>, V17)) end end end(E0, E1)); _ -> fun (V18) -> ('un--cantReify'('erased', 'erased', V6, <<"Visibility"/utf8>>, V18)) end end.
'case--reify-7028'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V10 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V11, V12) -> case V11 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V13, V14) -> case V14 of {'Idris.Core.Name.UN', E4} -> (fun (V15) -> case V15 of <<"I"/utf8>> -> case V12 of [E5 | E6] -> (fun (V16, V17) -> case V17 of [] -> fun (V18) -> begin (V22 = begin (V19 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V16))(V18))), case V19 of {'Idris.Prelude.Types.Left', E7} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V21) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V21))(V18)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V22 of {'Idris.Prelude.Types.Left', E9} -> (fun (V23) -> {'Idris.Prelude.Types.Left', V23} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V24) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.I', V24}} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V25) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V25)) end end end(E5, E6)); _ -> fun (V26) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V26)) end end; <<"BI"/utf8>> -> case V12 of [E11 | E12] -> (fun (V27, V28) -> case V28 of [] -> fun (V29) -> begin (V33 = begin (V30 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V27))(V29))), case V30 of {'Idris.Prelude.Types.Left', E13} -> (fun (V31) -> {'Idris.Prelude.Types.Left', V31} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V32) -> (('dn--un--reify_Reify__Integer'(V8, V0, V7, V32))(V29)) end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V33 of {'Idris.Prelude.Types.Left', E15} -> (fun (V34) -> {'Idris.Prelude.Types.Left', V34} end(E15)); {'Idris.Prelude.Types.Right', E16} -> (fun (V35) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.BI', V35}} end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V36) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V36)) end end end(E11, E12)); _ -> fun (V37) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V37)) end end; <<"B8"/utf8>> -> case V12 of [E17 | E18] -> (fun (V38, V39) -> case V39 of [] -> fun (V40) -> begin (V44 = begin (V41 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V38))(V40))), case V41 of {'Idris.Prelude.Types.Left', E19} -> (fun (V42) -> {'Idris.Prelude.Types.Left', V42} end(E19)); {'Idris.Prelude.Types.Right', E20} -> (fun (V43) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V43))(V40)) end(E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V44 of {'Idris.Prelude.Types.Left', E21} -> (fun (V45) -> {'Idris.Prelude.Types.Left', V45} end(E21)); {'Idris.Prelude.Types.Right', E22} -> (fun (V46) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.B8', V46}} end(E22)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V47) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V47)) end end end(E17, E18)); _ -> fun (V48) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V48)) end end; <<"B16"/utf8>> -> case V12 of [E23 | E24] -> (fun (V49, V50) -> case V50 of [] -> fun (V51) -> begin (V55 = begin (V52 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V49))(V51))), case V52 of {'Idris.Prelude.Types.Left', E25} -> (fun (V53) -> {'Idris.Prelude.Types.Left', V53} end(E25)); {'Idris.Prelude.Types.Right', E26} -> (fun (V54) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V54))(V51)) end(E26)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V55 of {'Idris.Prelude.Types.Left', E27} -> (fun (V56) -> {'Idris.Prelude.Types.Left', V56} end(E27)); {'Idris.Prelude.Types.Right', E28} -> (fun (V57) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.B16', V57}} end(E28)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V58) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V58)) end end end(E23, E24)); _ -> fun (V59) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V59)) end end; <<"B32"/utf8>> -> case V12 of [E29 | E30] -> (fun (V60, V61) -> case V61 of [] -> fun (V62) -> begin (V66 = begin (V63 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V60))(V62))), case V63 of {'Idris.Prelude.Types.Left', E31} -> (fun (V64) -> {'Idris.Prelude.Types.Left', V64} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V65) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V65))(V62)) end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V66 of {'Idris.Prelude.Types.Left', E33} -> (fun (V67) -> {'Idris.Prelude.Types.Left', V67} end(E33)); {'Idris.Prelude.Types.Right', E34} -> (fun (V68) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.B32', V68}} end(E34)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V69) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V69)) end end end(E29, E30)); _ -> fun (V70) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V70)) end end; <<"B64"/utf8>> -> case V12 of [E35 | E36] -> (fun (V71, V72) -> case V72 of [] -> fun (V73) -> begin (V77 = begin (V74 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V71))(V73))), case V74 of {'Idris.Prelude.Types.Left', E37} -> (fun (V75) -> {'Idris.Prelude.Types.Left', V75} end(E37)); {'Idris.Prelude.Types.Right', E38} -> (fun (V76) -> (('dn--un--reify_Reify__Integer'(V8, V0, V7, V76))(V73)) end(E38)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V77 of {'Idris.Prelude.Types.Left', E39} -> (fun (V78) -> {'Idris.Prelude.Types.Left', V78} end(E39)); {'Idris.Prelude.Types.Right', E40} -> (fun (V79) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.B64', V79}} end(E40)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V80) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V80)) end end end(E35, E36)); _ -> fun (V81) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V81)) end end; <<"Str"/utf8>> -> case V12 of [E41 | E42] -> (fun (V82, V83) -> case V83 of [] -> fun (V84) -> begin (V88 = begin (V85 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V82))(V84))), case V85 of {'Idris.Prelude.Types.Left', E43} -> (fun (V86) -> {'Idris.Prelude.Types.Left', V86} end(E43)); {'Idris.Prelude.Types.Right', E44} -> (fun (V87) -> (('dn--un--reify_Reify__String'(V8, V0, V7, V87))(V84)) end(E44)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V88 of {'Idris.Prelude.Types.Left', E45} -> (fun (V89) -> {'Idris.Prelude.Types.Left', V89} end(E45)); {'Idris.Prelude.Types.Right', E46} -> (fun (V90) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Str', V90}} end(E46)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V91) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V91)) end end end(E41, E42)); _ -> fun (V92) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V92)) end end; <<"Ch"/utf8>> -> case V12 of [E47 | E48] -> (fun (V93, V94) -> case V94 of [] -> fun (V95) -> begin (V99 = begin (V96 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V93))(V95))), case V96 of {'Idris.Prelude.Types.Left', E49} -> (fun (V97) -> {'Idris.Prelude.Types.Left', V97} end(E49)); {'Idris.Prelude.Types.Right', E50} -> (fun (V98) -> (('dn--un--reify_Reify__Char'(V8, V0, V7, V98))(V95)) end(E50)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V99 of {'Idris.Prelude.Types.Left', E51} -> (fun (V100) -> {'Idris.Prelude.Types.Left', V100} end(E51)); {'Idris.Prelude.Types.Right', E52} -> (fun (V101) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Ch', V101}} end(E52)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V102) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V102)) end end end(E47, E48)); _ -> fun (V103) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V103)) end end; <<"Db"/utf8>> -> case V12 of [E53 | E54] -> (fun (V104, V105) -> case V105 of [] -> fun (V106) -> begin (V110 = begin (V107 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V104))(V106))), case V107 of {'Idris.Prelude.Types.Left', E55} -> (fun (V108) -> {'Idris.Prelude.Types.Left', V108} end(E55)); {'Idris.Prelude.Types.Right', E56} -> (fun (V109) -> (('dn--un--reify_Reify__Double'(V8, V0, V7, V109))(V106)) end(E56)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V110 of {'Idris.Prelude.Types.Left', E57} -> (fun (V111) -> {'Idris.Prelude.Types.Left', V111} end(E57)); {'Idris.Prelude.Types.Right', E58} -> (fun (V112) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Db', V112}} end(E58)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V113) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V113)) end end end(E53, E54)); _ -> fun (V114) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V114)) end end; <<"WorldVal"/utf8>> -> case V12 of [] -> fun (V115) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.WorldVal'}} end; _ -> fun (V116) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V116)) end end; <<"IntType"/utf8>> -> case V12 of [] -> fun (V117) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.IntType'}} end; _ -> fun (V118) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V118)) end end; <<"IntegerType"/utf8>> -> case V12 of [] -> fun (V119) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.IntegerType'}} end; _ -> fun (V120) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V120)) end end; <<"Bits8Type"/utf8>> -> case V12 of [] -> fun (V121) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Bits8Type'}} end; _ -> fun (V122) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V122)) end end; <<"Bits16Type"/utf8>> -> case V12 of [] -> fun (V123) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Bits16Type'}} end; _ -> fun (V124) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V124)) end end; <<"Bits32Type"/utf8>> -> case V12 of [] -> fun (V125) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Bits32Type'}} end; _ -> fun (V126) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V126)) end end; <<"Bits64Type"/utf8>> -> case V12 of [] -> fun (V127) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Bits64Type'}} end; _ -> fun (V128) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V128)) end end; <<"StringType"/utf8>> -> case V12 of [] -> fun (V129) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.StringType'}} end; _ -> fun (V130) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V130)) end end; <<"CharType"/utf8>> -> case V12 of [] -> fun (V131) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.CharType'}} end; _ -> fun (V132) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V132)) end end; <<"DoubleType"/utf8>> -> case V12 of [] -> fun (V133) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.DoubleType'}} end; _ -> fun (V134) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V134)) end end; <<"WorldType"/utf8>> -> case V12 of [] -> fun (V135) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.WorldType'}} end; _ -> fun (V136) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V136)) end end; _ -> fun (V137) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V137)) end end end(E4)); _ -> fun (V138) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V138)) end end end(E2, E3)); _ -> fun (V139) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V139)) end end end(E0, E1)); _ -> fun (V140) -> ('un--cantReify'('erased', 'erased', V6, <<"Constant"/utf8>>, V140)) end end.
'case--reify-6623'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V10 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V11, V12) -> case V11 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V13, V14) -> case V14 of {'Idris.Core.Name.UN', E4} -> (fun (V15) -> case V15 of <<"Bound"/utf8>> -> fun (V16) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Bound'}} end; <<"Func"/utf8>> -> fun (V17) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Func'}} end; <<"DataCon"/utf8>> -> case V12 of [E5 | E6] -> (fun (V18, V19) -> case V19 of [E7 | E8] -> (fun (V20, V21) -> case V21 of [] -> fun (V22) -> begin (V26 = begin (V23 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V18))(V22))), case V23 of {'Idris.Prelude.Types.Left', E9} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V25) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V25))(V22)) end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V26 of {'Idris.Prelude.Types.Left', E11} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V28) -> begin (V32 = begin (V29 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V20))(V22))), case V29 of {'Idris.Prelude.Types.Left', E13} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V31) -> (('dn--un--reify_Reify__Nat'(V8, V0, V7, V31))(V22)) end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V32 of {'Idris.Prelude.Types.Left', E15} -> (fun (V33) -> {'Idris.Prelude.Types.Left', V33} end(E15)); {'Idris.Prelude.Types.Right', E16} -> (fun (V34) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.DataCon', V28, V34}} end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V35) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V35)) end end end(E7, E8)); _ -> fun (V36) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V36)) end end end(E5, E6)); _ -> fun (V37) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V37)) end end; <<"TyCon"/utf8>> -> case V12 of [E17 | E18] -> (fun (V38, V39) -> case V39 of [E19 | E20] -> (fun (V40, V41) -> case V41 of [] -> fun (V42) -> begin (V46 = begin (V43 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V38))(V42))), case V43 of {'Idris.Prelude.Types.Left', E21} -> (fun (V44) -> {'Idris.Prelude.Types.Left', V44} end(E21)); {'Idris.Prelude.Types.Right', E22} -> (fun (V45) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V45))(V42)) end(E22)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V46 of {'Idris.Prelude.Types.Left', E23} -> (fun (V47) -> {'Idris.Prelude.Types.Left', V47} end(E23)); {'Idris.Prelude.Types.Right', E24} -> (fun (V48) -> begin (V52 = begin (V49 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V40))(V42))), case V49 of {'Idris.Prelude.Types.Left', E25} -> (fun (V50) -> {'Idris.Prelude.Types.Left', V50} end(E25)); {'Idris.Prelude.Types.Right', E26} -> (fun (V51) -> (('dn--un--reify_Reify__Nat'(V8, V0, V7, V51))(V42)) end(E26)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V52 of {'Idris.Prelude.Types.Left', E27} -> (fun (V53) -> {'Idris.Prelude.Types.Left', V53} end(E27)); {'Idris.Prelude.Types.Right', E28} -> (fun (V54) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.TyCon', V48, V54}} end(E28)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E24)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V55) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V55)) end end end(E19, E20)); _ -> fun (V56) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V56)) end end end(E17, E18)); _ -> fun (V57) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V57)) end end; _ -> fun (V58) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V58)) end end end(E4)); _ -> fun (V59) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V59)) end end end(E2, E3)); _ -> fun (V60) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V60)) end end end(E0, E1)); _ -> fun (V61) -> ('un--cantReify'('erased', 'erased', V6, <<"NameType"/utf8>>, V61)) end end.
'case--reflect-6536'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Core.Name.Resolved', E0} -> (fun (V7) -> fun (V8) -> ('un--cantReflect'('erased', V5, <<"Name"/utf8>>, V8)) end end(E0)); _ -> ('dn--un--reflect_Reflect__Name'(V0, V5, V4, V3, V2, V6)) end.
'case--reify-6072'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V10 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V11, V12) -> case V11 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V13, V14) -> case V14 of {'Idris.Core.Name.UN', E4} -> (fun (V15) -> case V15 of <<"UN"/utf8>> -> case V12 of [E5 | E6] -> (fun (V16, V17) -> case V17 of [] -> fun (V18) -> begin (V22 = begin (V19 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V16))(V18))), case V19 of {'Idris.Prelude.Types.Left', E7} -> (fun (V20) -> {'Idris.Prelude.Types.Left', V20} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V21) -> (('dn--un--reify_Reify__String'(V8, V0, V7, V21))(V18)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V22 of {'Idris.Prelude.Types.Left', E9} -> (fun (V23) -> {'Idris.Prelude.Types.Left', V23} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V24) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Name.UN', V24}} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V25) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V25)) end end end(E5, E6)); _ -> fun (V26) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V26)) end end; <<"MN"/utf8>> -> case V12 of [E11 | E12] -> (fun (V27, V28) -> case V28 of [E13 | E14] -> (fun (V29, V30) -> case V30 of [] -> fun (V31) -> begin (V35 = begin (V32 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V27))(V31))), case V32 of {'Idris.Prelude.Types.Left', E15} -> (fun (V33) -> {'Idris.Prelude.Types.Left', V33} end(E15)); {'Idris.Prelude.Types.Right', E16} -> (fun (V34) -> (('dn--un--reify_Reify__String'(V8, V0, V7, V34))(V31)) end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V35 of {'Idris.Prelude.Types.Left', E17} -> (fun (V36) -> {'Idris.Prelude.Types.Left', V36} end(E17)); {'Idris.Prelude.Types.Right', E18} -> (fun (V37) -> begin (V41 = begin (V38 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V29))(V31))), case V38 of {'Idris.Prelude.Types.Left', E19} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E19)); {'Idris.Prelude.Types.Right', E20} -> (fun (V40) -> (('dn--un--reify_Reify__Int'(V8, V0, V7, V40))(V31)) end(E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V41 of {'Idris.Prelude.Types.Left', E21} -> (fun (V42) -> {'Idris.Prelude.Types.Left', V42} end(E21)); {'Idris.Prelude.Types.Right', E22} -> (fun (V43) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Name.MN', V37, V43}} end(E22)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V44) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V44)) end end end(E13, E14)); _ -> fun (V45) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V45)) end end end(E11, E12)); _ -> fun (V46) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V46)) end end; <<"NS"/utf8>> -> case V12 of [E23 | E24] -> (fun (V47, V48) -> case V48 of [E25 | E26] -> (fun (V49, V50) -> case V50 of [] -> fun (V51) -> begin (V55 = begin (V52 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V47))(V51))), case V52 of {'Idris.Prelude.Types.Left', E27} -> (fun (V53) -> {'Idris.Prelude.Types.Left', V53} end(E27)); {'Idris.Prelude.Types.Right', E28} -> (fun (V54) -> (('dn--un--reify_Reify__Namespace'(V8, V0, V7, V54))(V51)) end(E28)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V55 of {'Idris.Prelude.Types.Left', E29} -> (fun (V56) -> {'Idris.Prelude.Types.Left', V56} end(E29)); {'Idris.Prelude.Types.Right', E30} -> (fun (V57) -> begin (V61 = begin (V58 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V49))(V51))), case V58 of {'Idris.Prelude.Types.Left', E31} -> (fun (V59) -> {'Idris.Prelude.Types.Left', V59} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V60) -> (('dn--un--reify_Reify__Name'(V8, V0, V7, V60))(V51)) end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V61 of {'Idris.Prelude.Types.Left', E33} -> (fun (V62) -> {'Idris.Prelude.Types.Left', V62} end(E33)); {'Idris.Prelude.Types.Right', E34} -> (fun (V63) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Name.NS', V57, V63}} end(E34)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V64) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V64)) end end end(E25, E26)); _ -> fun (V65) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V65)) end end end(E23, E24)); _ -> fun (V66) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V66)) end end; <<"DN"/utf8>> -> case V12 of [E35 | E36] -> (fun (V67, V68) -> case V68 of [E37 | E38] -> (fun (V69, V70) -> case V70 of [] -> fun (V71) -> begin (V75 = begin (V72 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V67))(V71))), case V72 of {'Idris.Prelude.Types.Left', E39} -> (fun (V73) -> {'Idris.Prelude.Types.Left', V73} end(E39)); {'Idris.Prelude.Types.Right', E40} -> (fun (V74) -> (('dn--un--reify_Reify__String'(V8, V0, V7, V74))(V71)) end(E40)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V75 of {'Idris.Prelude.Types.Left', E41} -> (fun (V76) -> {'Idris.Prelude.Types.Left', V76} end(E41)); {'Idris.Prelude.Types.Right', E42} -> (fun (V77) -> begin (V81 = begin (V78 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V69))(V71))), case V78 of {'Idris.Prelude.Types.Left', E43} -> (fun (V79) -> {'Idris.Prelude.Types.Left', V79} end(E43)); {'Idris.Prelude.Types.Right', E44} -> (fun (V80) -> (('dn--un--reify_Reify__Name'(V8, V0, V7, V80))(V71)) end(E44)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V81 of {'Idris.Prelude.Types.Left', E45} -> (fun (V82) -> {'Idris.Prelude.Types.Left', V82} end(E45)); {'Idris.Prelude.Types.Right', E46} -> (fun (V83) -> {'Idris.Prelude.Types.Right', {'Idris.Core.Name.DN', V77, V83}} end(E46)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V84) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V84)) end end end(E37, E38)); _ -> fun (V85) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V85)) end end end(E35, E36)); _ -> fun (V86) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V86)) end end; _ -> fun (V87) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V87)) end end end(E4)); _ -> fun (V88) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V88)) end end end(E2, E3)); _ -> fun (V89) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V89)) end end end(E0, E1)); _ -> fun (V90) -> ('un--cantReify'('erased', 'erased', V6, <<"Name"/utf8>>, V90)) end end.
'case--reify-5894'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.Name.UN', E2} -> (fun (V12) -> case V12 of <<"MkNS"/utf8>> -> fun (V13) -> begin (V21 = begin (V14 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V4))(V13))), case V14 of {'Idris.Prelude.Types.Left', E3} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V16) -> (('dn--un--reify_Reify__(List $a)'('erased', fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> ('dn--un--reify_Reify__String'(V17, V18, V19, V20)) end end end end, V8, V0, V7, V16))(V13)) end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V21 of {'Idris.Prelude.Types.Left', E5} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V23) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Core.Name.Namespace':'un--unsafeFoldNamespace'(V23))} end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V24) -> ('un--cantReify'('erased', 'erased', V6, <<"Namespace"/utf8>>, V24)) end end end(E2)); _ -> fun (V25) -> ('un--cantReify'('erased', 'erased', V6, <<"Namespace"/utf8>>, V25)) end end end(E0, E1)); _ -> fun (V26) -> ('un--cantReify'('erased', 'erased', V6, <<"Namespace"/utf8>>, V26)) end end.
'case--reify-5642'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15) -> case V15 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V16, V17) -> case V17 of {'Idris.Core.Name.UN', E2} -> (fun (V18) -> case V18 of <<"MkPair"/utf8>> -> fun (V19) -> begin (V23 = begin (V20 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V14, V3, V13, V9))(V19))), case V20 of {'Idris.Prelude.Types.Left', E3} -> (fun (V21) -> {'Idris.Prelude.Types.Left', V21} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V22) -> (((((('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V2))(V14))(V3))(V13))(V22))(V19)) end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V23 of {'Idris.Prelude.Types.Left', E5} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V25) -> begin (V29 = begin (V26 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V14, V3, V13, V10))(V19))), case V26 of {'Idris.Prelude.Types.Left', E7} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V28) -> (((((('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V2))(V14))(V3))(V13))(V28))(V19)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V29 of {'Idris.Prelude.Types.Left', E9} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V31) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', V25, V31}} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V32) -> ('un--cantReify'('erased', 'erased', V12, <<"Pair"/utf8>>, V32)) end end end(E2)); _ -> fun (V33) -> ('un--cantReify'('erased', 'erased', V12, <<"Pair"/utf8>>, V33)) end end end(E0, E1)); _ -> fun (V34) -> ('un--cantReify'('erased', 'erased', V12, <<"Pair"/utf8>>, V34)) end end.
'case--reify-5346'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V13, V14) -> case V13 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V15, V16) -> case V16 of {'Idris.Core.Name.UN', E4} -> (fun (V17) -> case V17 of <<"Nothing"/utf8>> -> fun (V18) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Nothing'}} end; <<"Just"/utf8>> -> case V14 of [E5 | E6] -> (fun (V19, V20) -> case V20 of [E7 | E8] -> (fun (V21, V22) -> case V22 of [] -> fun (V23) -> begin (V27 = begin (V24 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V10, V2, V9, V21))(V23))), case V24 of {'Idris.Prelude.Types.Left', E9} -> (fun (V25) -> {'Idris.Prelude.Types.Left', V25} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V26) -> (((((V1(V10))(V2))(V9))(V26))(V23)) end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V27 of {'Idris.Prelude.Types.Left', E11} -> (fun (V28) -> {'Idris.Prelude.Types.Left', V28} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V29) -> {'Idris.Prelude.Types.Right', {'Idris.Prelude.Types.Just', V29}} end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V30) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V30)) end end end(E7, E8)); _ -> fun (V31) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V31)) end end end(E5, E6)); _ -> fun (V32) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V32)) end end; _ -> fun (V33) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V33)) end end end(E4)); _ -> fun (V34) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V34)) end end end(E2, E3)); _ -> fun (V35) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V35)) end end end(E0, E1)); _ -> fun (V36) -> ('un--cantReify'('erased', 'erased', V8, <<"Maybe"/utf8>>, V36)) end end.
'case--reify-5096'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12, V13) -> case V13 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V14, V15) -> case V15 of {'Idris.Core.Name.UN', E2} -> (fun (V16) -> case V16 of <<":::"/utf8>> -> fun (V17) -> begin (V21 = begin (V18 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V12, V2, V11, V7))(V17))), case V18 of {'Idris.Prelude.Types.Left', E3} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V20) -> (((((V1(V12))(V2))(V11))(V20))(V17)) end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V21 of {'Idris.Prelude.Types.Left', E5} -> (fun (V22) -> {'Idris.Prelude.Types.Left', V22} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V23) -> begin (V27 = begin (V24 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V12, V2, V11, V8))(V17))), case V24 of {'Idris.Prelude.Types.Left', E7} -> (fun (V25) -> {'Idris.Prelude.Types.Left', V25} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V26) -> (('dn--un--reify_Reify__(List $a)'('erased', V1, V12, V2, V11, V26))(V17)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V27 of {'Idris.Prelude.Types.Left', E9} -> (fun (V28) -> {'Idris.Prelude.Types.Left', V28} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V29) -> {'Idris.Prelude.Types.Right', {'Idris.Data.List1.:::', V23, V29}} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V30) -> ('un--cantReify'('erased', 'erased', V10, <<"List1"/utf8>>, V30)) end end end(E2)); _ -> fun (V31) -> ('un--cantReify'('erased', 'erased', V10, <<"List1"/utf8>>, V31)) end end end(E0, E1)); _ -> fun (V32) -> ('un--cantReify'('erased', 'erased', V10, <<"List1"/utf8>>, V32)) end end.
'case--reify-4770'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10, V11, V12) -> case V12 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V13, V14) -> case V13 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V15, V16) -> case V16 of {'Idris.Core.Name.UN', E4} -> (fun (V17) -> case V17 of <<"Nil"/utf8>> -> fun (V18) -> {'Idris.Prelude.Types.Right', []} end; <<"::"/utf8>> -> case V14 of [E5 | E6] -> (fun (V19, V20) -> case V20 of [E7 | E8] -> (fun (V21, V22) -> case V22 of [E9 | E10] -> (fun (V23, V24) -> case V24 of [] -> fun (V25) -> begin (V29 = begin (V26 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V10, V2, V9, V21))(V25))), case V26 of {'Idris.Prelude.Types.Left', E11} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V28) -> (((((V1(V10))(V2))(V9))(V28))(V25)) end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V29 of {'Idris.Prelude.Types.Left', E13} -> (fun (V30) -> {'Idris.Prelude.Types.Left', V30} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V31) -> begin (V35 = begin (V32 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V10, V2, V9, V23))(V25))), case V32 of {'Idris.Prelude.Types.Left', E15} -> (fun (V33) -> {'Idris.Prelude.Types.Left', V33} end(E15)); {'Idris.Prelude.Types.Right', E16} -> (fun (V34) -> (('dn--un--reify_Reify__(List $a)'('erased', V1, V10, V2, V9, V34))(V25)) end(E16)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V35 of {'Idris.Prelude.Types.Left', E17} -> (fun (V36) -> {'Idris.Prelude.Types.Left', V36} end(E17)); {'Idris.Prelude.Types.Right', E18} -> (fun (V37) -> {'Idris.Prelude.Types.Right', [V31 | V37]} end(E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V38) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V38)) end end end(E9, E10)); _ -> fun (V39) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V39)) end end end(E7, E8)); _ -> fun (V40) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V40)) end end end(E5, E6)); _ -> fun (V41) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V41)) end end; _ -> fun (V42) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V42)) end end end(E4)); _ -> fun (V43) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V43)) end end end(E2, E3)); _ -> fun (V44) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V44)) end end end(E0, E1)); _ -> fun (V45) -> ('un--cantReify'('erased', 'erased', V8, <<"List"/utf8>>, V45)) end end.
'case--reify-4529'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V10 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V11, V12) -> case V11 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V13, V14) -> case V14 of {'Idris.Core.Name.UN', E4} -> (fun (V15) -> case V15 of <<"Z"/utf8>> -> fun (V16) -> {'Idris.Prelude.Types.Right', 0} end; <<"S"/utf8>> -> case V12 of [E5 | E6] -> (fun (V17, V18) -> case V18 of [] -> fun (V19) -> begin (V23 = begin (V20 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V8, V0, V7, V17))(V19))), case V20 of {'Idris.Prelude.Types.Left', E7} -> (fun (V21) -> {'Idris.Prelude.Types.Left', V21} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V22) -> (('dn--un--reify_Reify__Nat'(V8, V0, V7, V22))(V19)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V23 of {'Idris.Prelude.Types.Left', E9} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E9)); {'Idris.Prelude.Types.Right', E10} -> (fun (V25) -> {'Idris.Prelude.Types.Right', (1 + V25)} end(E10)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V26) -> ('un--cantReify'('erased', 'erased', V6, <<"Nat"/utf8>>, V26)) end end end(E5, E6)); _ -> fun (V27) -> ('un--cantReify'('erased', 'erased', V6, <<"Nat"/utf8>>, V27)) end end; _ -> fun (V28) -> ('un--cantReify'('erased', 'erased', V6, <<"Nat"/utf8>>, V28)) end end end(E4)); _ -> fun (V29) -> ('un--cantReify'('erased', 'erased', V6, <<"Nat"/utf8>>, V29)) end end end(E2, E3)); _ -> fun (V30) -> ('un--cantReify'('erased', 'erased', V6, <<"Nat"/utf8>>, V30)) end end end(E0, E1)); _ -> fun (V31) -> ('un--cantReify'('erased', 'erased', V6, <<"Nat"/utf8>>, V31)) end end.
'case--reify-4352'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9) -> case V9 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V10, V11) -> case V11 of {'Idris.Core.Name.UN', E2} -> (fun (V12) -> case V12 of <<"True"/utf8>> -> fun (V13) -> {'Idris.Prelude.Types.Right', 0} end; <<"False"/utf8>> -> fun (V14) -> {'Idris.Prelude.Types.Right', 1} end; _ -> fun (V15) -> ('un--cantReify'('erased', 'erased', V6, <<"Bool"/utf8>>, V15)) end end end(E2)); _ -> fun (V16) -> ('un--cantReify'('erased', 'erased', V6, <<"Bool"/utf8>>, V16)) end end end(E0, E1)); _ -> fun (V17) -> ('un--cantReify'('erased', 'erased', V6, <<"Bool"/utf8>>, V17)) end end.
'case--getCon-3721'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Prelude.Types.Just', E0} -> (fun (V5) -> case V5 of {'Idris.Core.Context.DCon', E27, E28, E29} -> (fun (V6, V7, V8) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54, E55} -> (fun (V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34) -> V9 end(E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54, E55)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.TT.Ref', V3, {'Idris.Core.TT.DataCon', V6, V7}, V1})) end(E27, E28, E29)); {'Idris.Core.Context.TCon', E56, E57, E58, E59, E60, E61, E62, E63} -> (fun (V35, V36, V37, V38, V39, V40, V41, V42) -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81, E82, E83, E84, E85, E86, E87, E88, E89} -> (fun (V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63, V64, V65, V66, V67, V68) -> V43 end(E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81, E82, E83, E84, E85, E86, E87, E88, E89)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.TT.Ref', V3, {'Idris.Core.TT.TyCon', V35, V36}, V1})) end(E56, E57, E58, E59, E60, E61, E62, E63)); _ -> ('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26} -> (fun (V69, V70, V71, V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85, V86, V87, V88, V89, V90, V91, V92, V93, V94) -> V69 end(E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.TT.Ref', V3, {'Idris.Core.TT.Func'}, V1})) end end(E0)); _ -> fun (V95) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V3, V1}, V95)) end end.
'dn--un--reify_Reify__Visibility'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), case V38 of {'Idris.Core.Name.NS', E33, E34} -> (fun (V40, V41) -> case V41 of {'Idris.Core.Name.UN', E35} -> (fun (V42) -> case V42 of <<"Private"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Private'}}; <<"Export"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Export'}}; <<"Public"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Public'}}; _ -> ('un--cantReify'('erased', 'erased', V39, <<"Visibility"/utf8>>, V9)) end end(E35)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"Visibility"/utf8>>, V9)) end end(E33, E34)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"Visibility"/utf8>>, V9)) end end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V43) -> ('un--cantReify'('erased', 'erased', V3, <<"Visibility"/utf8>>, V43)) end end.
'dn--un--reify_Reify__TotalReq'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), case V38 of {'Idris.Core.Name.NS', E33, E34} -> (fun (V40, V41) -> case V41 of {'Idris.Core.Name.UN', E35} -> (fun (V42) -> case V42 of <<"Total"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Total'}}; <<"CoveringOnly"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.CoveringOnly'}}; <<"PartialOK"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PartialOK'}}; _ -> ('un--cantReify'('erased', 'erased', V39, <<"TotalReq"/utf8>>, V9)) end end(E35)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"TotalReq"/utf8>>, V9)) end end(E33, E34)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"TotalReq"/utf8>>, V9)) end end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V43) -> ('un--cantReify'('erased', 'erased', V3, <<"TotalReq"/utf8>>, V43)) end end.
'dn--un--reify_Reify__String'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NPrimVal', E0, E1} -> (fun (V4, V5) -> case V5 of {'Idris.Core.TT.Str', E2} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E2)); _ -> fun (V8) -> ('un--cantReify'('erased', 'erased', V3, <<"String"/utf8>>, V8)) end end end(E0, E1)); _ -> fun (V9) -> ('un--cantReify'('erased', 'erased', V3, <<"String"/utf8>>, V9)) end end.
'dn--un--reify_Reify__RigCount'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), case V38 of {'Idris.Core.Name.NS', E33, E34} -> (fun (V40, V41) -> case V41 of {'Idris.Core.Name.UN', E35} -> (fun (V42) -> case V42 of <<"M0"/utf8>> -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V43) -> fun (V44) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V43, V44)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V45) -> fun (V46) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V45, V46)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))}; <<"M1"/utf8>> -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.Semiring':'un--linear'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V47) -> fun (V48) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V47, V48)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V49) -> fun (V50) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V49, V50)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}))}; <<"MW"/utf8>> -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--top_Top__ZeroOneOmega'())}; _ -> ('un--cantReify'('erased', 'erased', V39, <<"Count"/utf8>>, V9)) end end(E35)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"Count"/utf8>>, V9)) end end(E33, E34)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"Count"/utf8>>, V9)) end end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V51) -> ('un--cantReify'('erased', 'erased', V3, <<"Count"/utf8>>, V51)) end end.
'dn--un--reify_Reify__Nat'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), (('case--reify-4529'(V1, V4, V6, V7, V8, V5, V39, V2, V0, V38, {'Idris.Builtin.MkPair', V38, V8}))(V9)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V40) -> ('un--cantReify'('erased', 'erased', V3, <<"Nat"/utf8>>, V40)) end end.
'dn--un--reify_Reify__Namespace'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> case V8 of [E5 | E6] -> (fun (V9, V10) -> case V10 of [] -> fun (V11) -> begin (V38 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32} -> (fun (V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37) -> V12 end(E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V11))), case V38 of {'Idris.Prelude.Types.Left', E33} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E33)); {'Idris.Prelude.Types.Right', E34} -> (fun (V40) -> begin (V41 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, [V9 | []]}), case V40 of {'Idris.Core.Name.NS', E35, E36} -> (fun (V42, V43) -> case V43 of {'Idris.Core.Name.UN', E37} -> (fun (V44) -> case V44 of <<"MkNS"/utf8>> -> begin (V52 = begin (V45 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V0, V1, V2, V9))(V11))), case V45 of {'Idris.Prelude.Types.Left', E38} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E38)); {'Idris.Prelude.Types.Right', E39} -> (fun (V47) -> (('dn--un--reify_Reify__(List $a)'('erased', fun (V48) -> fun (V49) -> fun (V50) -> fun (V51) -> ('dn--un--reify_Reify__String'(V48, V49, V50, V51)) end end end end, V0, V1, V2, V47))(V11)) end(E39)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V52 of {'Idris.Prelude.Types.Left', E40} -> (fun (V53) -> {'Idris.Prelude.Types.Left', V53} end(E40)); {'Idris.Prelude.Types.Right', E41} -> (fun (V54) -> {'Idris.Prelude.Types.Right', ('Idris.Idris2.Core.Name.Namespace':'un--unsafeFoldNamespace'(V54))} end(E41)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; _ -> ('un--cantReify'('erased', 'erased', V41, <<"Namespace"/utf8>>, V11)) end end(E37)); _ -> ('un--cantReify'('erased', 'erased', V41, <<"Namespace"/utf8>>, V11)) end end(E35, E36)); _ -> ('un--cantReify'('erased', 'erased', V41, <<"Namespace"/utf8>>, V11)) end end end(E34)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V55) -> ('un--cantReify'('erased', 'erased', V3, <<"Namespace"/utf8>>, V55)) end end end(E5, E6)); _ -> fun (V56) -> ('un--cantReify'('erased', 'erased', V3, <<"Namespace"/utf8>>, V56)) end end end(E0, E1, E2, E3, E4)); _ -> fun (V57) -> ('un--cantReify'('erased', 'erased', V3, <<"Namespace"/utf8>>, V57)) end end.
'dn--un--reify_Reify__NameType'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), (('case--reify-6623'(V1, V4, V6, V7, V8, V5, V39, V2, V0, V38, {'Idris.Builtin.MkPair', V38, V8}))(V9)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V40) -> ('un--cantReify'('erased', 'erased', V3, <<"NameType"/utf8>>, V40)) end end.
'dn--un--reify_Reify__Name'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), (('case--reify-6072'(V1, V4, V6, V7, V8, V5, V39, V2, V0, V38, {'Idris.Builtin.MkPair', V38, V8}))(V9)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V40) -> ('un--cantReify'('erased', 'erased', V3, <<"Name"/utf8>>, V40)) end end.
'dn--un--reify_Reify__LazyReason'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), case V38 of {'Idris.Core.Name.NS', E33, E34} -> (fun (V40, V41) -> case V41 of {'Idris.Core.Name.UN', E35} -> (fun (V42) -> case V42 of <<"LInf"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.LInf'}}; <<"LLazy"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.LLazy'}}; <<"LUnknown"/utf8>> -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.LUnknown'}}; _ -> ('un--cantReify'('erased', 'erased', V39, <<"LazyReason"/utf8>>, V9)) end end(E35)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"LazyReason"/utf8>>, V9)) end end(E33, E34)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"LazyReason"/utf8>>, V9)) end end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V43) -> ('un--cantReify'('erased', 'erased', V3, <<"LazyReason"/utf8>>, V43)) end end.
'dn--un--reify_Reify__Integer'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NPrimVal', E0, E1} -> (fun (V4, V5) -> case V5 of {'Idris.Core.TT.BI', E2} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E2)); _ -> fun (V8) -> ('un--cantReify'('erased', 'erased', V3, <<"Integer"/utf8>>, V8)) end end end(E0, E1)); _ -> fun (V9) -> ('un--cantReify'('erased', 'erased', V3, <<"Integer"/utf8>>, V9)) end end.
'dn--un--reify_Reify__Int'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NPrimVal', E0, E1} -> (fun (V4, V5) -> case V5 of {'Idris.Core.TT.I', E2} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E2)); _ -> fun (V8) -> ('un--cantReify'('erased', 'erased', V3, <<"Int"/utf8>>, V8)) end end end(E0, E1)); _ -> fun (V9) -> ('un--cantReify'('erased', 'erased', V3, <<"Int"/utf8>>, V9)) end end.
'dn--un--reify_Reify__FC'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), (('case--reify-9472'(V1, V4, V6, V7, V8, V5, V39, V2, V0, V38, {'Idris.Builtin.MkPair', V38, V8}))(V9)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V40) -> ('un--cantReify'('erased', 'erased', V3, <<"FC"/utf8>>, V40)) end end.
'dn--un--reify_Reify__Double'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NPrimVal', E0, E1} -> (fun (V4, V5) -> case V5 of {'Idris.Core.TT.Db', E2} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E2)); _ -> fun (V8) -> ('un--cantReify'('erased', 'erased', V3, <<"Double"/utf8>>, V8)) end end end(E0, E1)); _ -> fun (V9) -> ('un--cantReify'('erased', 'erased', V3, <<"Double"/utf8>>, V9)) end end.
'dn--un--reify_Reify__Constant'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), (('case--reify-7028'(V1, V4, V6, V7, V8, V5, V39, V2, V0, V38, {'Idris.Builtin.MkPair', V38, V8}))(V9)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V40) -> ('un--cantReify'('erased', 'erased', V3, <<"Constant"/utf8>>, V40)) end end.
'dn--un--reify_Reify__Char'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NPrimVal', E0, E1} -> (fun (V4, V5) -> case V5 of {'Idris.Core.TT.Ch', E2} -> (fun (V6) -> fun (V7) -> {'Idris.Prelude.Types.Right', V6} end end(E2)); _ -> fun (V8) -> ('un--cantReify'('erased', 'erased', V3, <<"Char"/utf8>>, V8)) end end end(E0, E1)); _ -> fun (V9) -> ('un--cantReify'('erased', 'erased', V3, <<"Char"/utf8>>, V9)) end end.
'dn--un--reify_Reify__Bool'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V4, V5, V6, V7, V8) -> fun (V9) -> begin (V36 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35) -> V10 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V5))(V9))), case V36 of {'Idris.Prelude.Types.Left', E31} -> (fun (V37) -> {'Idris.Prelude.Types.Left', V37} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V38) -> begin (V39 = {'Idris.Core.Value.NDCon', V4, V5, V6, V7, V8}), case V38 of {'Idris.Core.Name.NS', E33, E34} -> (fun (V40, V41) -> case V41 of {'Idris.Core.Name.UN', E35} -> (fun (V42) -> case V42 of <<"True"/utf8>> -> {'Idris.Prelude.Types.Right', 0}; <<"False"/utf8>> -> {'Idris.Prelude.Types.Right', 1}; _ -> ('un--cantReify'('erased', 'erased', V39, <<"Bool"/utf8>>, V9)) end end(E35)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"Bool"/utf8>>, V9)) end end(E33, E34)); _ -> ('un--cantReify'('erased', 'erased', V39, <<"Bool"/utf8>>, V9)) end end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V43) -> ('un--cantReify'('erased', 'erased', V3, <<"Bool"/utf8>>, V43)) end end.
'dn--un--reify_Reify__(|Unit,MkUnit|)'(V0, V1, V2, V3, V4) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkUnit'}}.
'dn--un--reify_Reify__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V7, V8, V9, V10, V11) -> case V11 of [E5 | E6] -> (fun (V12, V13) -> case V13 of [E7 | E8] -> (fun (V14, V15) -> case V15 of [E9 | E10] -> (fun (V16, V17) -> case V17 of [E11 | E12] -> (fun (V18, V19) -> case V19 of [] -> fun (V20) -> begin (V47 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V5 of {'Idris.Core.Context.MkDefs', E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38} -> (fun (V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37, V38, V39, V40, V41, V42, V43, V44, V45, V46) -> V21 end(E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V8))(V20))), case V47 of {'Idris.Prelude.Types.Left', E39} -> (fun (V48) -> {'Idris.Prelude.Types.Left', V48} end(E39)); {'Idris.Prelude.Types.Right', E40} -> (fun (V49) -> begin (V50 = {'Idris.Core.Value.NDCon', V7, V8, V9, V10, [V12 | [V14 | [V16 | [V18 | []]]]]}), case V49 of {'Idris.Core.Name.NS', E41, E42} -> (fun (V51, V52) -> case V52 of {'Idris.Core.Name.UN', E43} -> (fun (V53) -> case V53 of <<"MkPair"/utf8>> -> begin (V57 = begin (V54 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V3, V4, V5, V16))(V20))), case V54 of {'Idris.Prelude.Types.Left', E44} -> (fun (V55) -> {'Idris.Prelude.Types.Left', V55} end(E44)); {'Idris.Prelude.Types.Right', E45} -> (fun (V56) -> (((((('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V2))(V3))(V4))(V5))(V56))(V20)) end(E45)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V57 of {'Idris.Prelude.Types.Left', E46} -> (fun (V58) -> {'Idris.Prelude.Types.Left', V58} end(E46)); {'Idris.Prelude.Types.Right', E47} -> (fun (V59) -> begin (V63 = begin (V60 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V3, V4, V5, V18))(V20))), case V60 of {'Idris.Prelude.Types.Left', E48} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E48)); {'Idris.Prelude.Types.Right', E49} -> (fun (V62) -> (((((('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V2))(V3))(V4))(V5))(V62))(V20)) end(E49)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V63 of {'Idris.Prelude.Types.Left', E50} -> (fun (V64) -> {'Idris.Prelude.Types.Left', V64} end(E50)); {'Idris.Prelude.Types.Right', E51} -> (fun (V65) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', V59, V65}} end(E51)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E47)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; _ -> ('un--cantReify'('erased', 'erased', V50, <<"Pair"/utf8>>, V20)) end end(E43)); _ -> ('un--cantReify'('erased', 'erased', V50, <<"Pair"/utf8>>, V20)) end end(E41, E42)); _ -> ('un--cantReify'('erased', 'erased', V50, <<"Pair"/utf8>>, V20)) end end end(E40)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V66) -> ('un--cantReify'('erased', 'erased', V6, <<"Pair"/utf8>>, V66)) end end end(E11, E12)); _ -> fun (V67) -> ('un--cantReify'('erased', 'erased', V6, <<"Pair"/utf8>>, V67)) end end end(E9, E10)); _ -> fun (V68) -> ('un--cantReify'('erased', 'erased', V6, <<"Pair"/utf8>>, V68)) end end end(E7, E8)); _ -> fun (V69) -> ('un--cantReify'('erased', 'erased', V6, <<"Pair"/utf8>>, V69)) end end end(E5, E6)); _ -> fun (V70) -> ('un--cantReify'('erased', 'erased', V6, <<"Pair"/utf8>>, V70)) end end end(E0, E1, E2, E3, E4)); _ -> fun (V71) -> ('un--cantReify'('erased', 'erased', V6, <<"Pair"/utf8>>, V71)) end end.
'dn--un--reify_Reify__(PiInfo $t)'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V6, V7, V8, V9, V10) -> fun (V11) -> begin (V38 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V4 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37) -> V12 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V7))(V11))), case V38 of {'Idris.Prelude.Types.Left', E31} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V40) -> begin (V41 = {'Idris.Core.Value.NDCon', V6, V7, V8, V9, V10}), (('case--reify-8883'('erased', V1, V3, V6, V8, V9, V10, V7, V41, V4, V2, V40, {'Idris.Builtin.MkPair', V40, V10}))(V11)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V42) -> ('un--cantReify'('erased', 'erased', V5, <<"PiInfo"/utf8>>, V42)) end end.
'dn--un--reify_Reify__(Maybe $a)'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V6, V7, V8, V9, V10) -> fun (V11) -> begin (V38 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V4 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37) -> V12 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V7))(V11))), case V38 of {'Idris.Prelude.Types.Left', E31} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V40) -> begin (V41 = {'Idris.Core.Value.NDCon', V6, V7, V8, V9, V10}), (('case--reify-5346'('erased', V1, V3, V6, V8, V9, V10, V7, V41, V4, V2, V40, {'Idris.Builtin.MkPair', V40, V10}))(V11)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V42) -> ('un--cantReify'('erased', 'erased', V5, <<"Maybe"/utf8>>, V42)) end end.
'dn--un--reify_Reify__(List1 $a)'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V6, V7, V8, V9, V10) -> case V10 of [E5 | E6] -> (fun (V11, V12) -> case V12 of [E7 | E8] -> (fun (V13, V14) -> case V14 of [E9 | E10] -> (fun (V15, V16) -> case V16 of [] -> fun (V17) -> begin (V44 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V4 of {'Idris.Core.Context.MkDefs', E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36} -> (fun (V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37, V38, V39, V40, V41, V42, V43) -> V18 end(E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V7))(V17))), case V44 of {'Idris.Prelude.Types.Left', E37} -> (fun (V45) -> {'Idris.Prelude.Types.Left', V45} end(E37)); {'Idris.Prelude.Types.Right', E38} -> (fun (V46) -> begin (V47 = {'Idris.Core.Value.NDCon', V6, V7, V8, V9, [V11 | [V13 | [V15 | []]]]}), case V46 of {'Idris.Core.Name.NS', E39, E40} -> (fun (V48, V49) -> case V49 of {'Idris.Core.Name.UN', E41} -> (fun (V50) -> case V50 of <<":::"/utf8>> -> begin (V54 = begin (V51 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V2, V3, V4, V13))(V17))), case V51 of {'Idris.Prelude.Types.Left', E42} -> (fun (V52) -> {'Idris.Prelude.Types.Left', V52} end(E42)); {'Idris.Prelude.Types.Right', E43} -> (fun (V53) -> (((((V1(V2))(V3))(V4))(V53))(V17)) end(E43)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V54 of {'Idris.Prelude.Types.Left', E44} -> (fun (V55) -> {'Idris.Prelude.Types.Left', V55} end(E44)); {'Idris.Prelude.Types.Right', E45} -> (fun (V56) -> begin (V60 = begin (V57 = (('Idris.Idris2.Core.Normalise':'un--evalClosure'(V2, V3, V4, V15))(V17))), case V57 of {'Idris.Prelude.Types.Left', E46} -> (fun (V58) -> {'Idris.Prelude.Types.Left', V58} end(E46)); {'Idris.Prelude.Types.Right', E47} -> (fun (V59) -> (('dn--un--reify_Reify__(List $a)'('erased', V1, V2, V3, V4, V59))(V17)) end(E47)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end), case V60 of {'Idris.Prelude.Types.Left', E48} -> (fun (V61) -> {'Idris.Prelude.Types.Left', V61} end(E48)); {'Idris.Prelude.Types.Right', E49} -> (fun (V62) -> {'Idris.Prelude.Types.Right', {'Idris.Data.List1.:::', V56, V62}} end(E49)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E45)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; _ -> ('un--cantReify'('erased', 'erased', V47, <<"List1"/utf8>>, V17)) end end(E41)); _ -> ('un--cantReify'('erased', 'erased', V47, <<"List1"/utf8>>, V17)) end end(E39, E40)); _ -> ('un--cantReify'('erased', 'erased', V47, <<"List1"/utf8>>, V17)) end end end(E38)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end; _ -> fun (V63) -> ('un--cantReify'('erased', 'erased', V5, <<"List1"/utf8>>, V63)) end end end(E9, E10)); _ -> fun (V64) -> ('un--cantReify'('erased', 'erased', V5, <<"List1"/utf8>>, V64)) end end end(E7, E8)); _ -> fun (V65) -> ('un--cantReify'('erased', 'erased', V5, <<"List1"/utf8>>, V65)) end end end(E5, E6)); _ -> fun (V66) -> ('un--cantReify'('erased', 'erased', V5, <<"List1"/utf8>>, V66)) end end end(E0, E1, E2, E3, E4)); _ -> fun (V67) -> ('un--cantReify'('erased', 'erased', V5, <<"List1"/utf8>>, V67)) end end.
'dn--un--reify_Reify__(List $a)'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Value.NDCon', E0, E1, E2, E3, E4} -> (fun (V6, V7, V8, V9, V10) -> fun (V11) -> begin (V38 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V4 of {'Idris.Core.Context.MkDefs', E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30} -> (fun (V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34, V35, V36, V37) -> V12 end(E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27, E28, E29, E30)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V7))(V11))), case V38 of {'Idris.Prelude.Types.Left', E31} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E31)); {'Idris.Prelude.Types.Right', E32} -> (fun (V40) -> begin (V41 = {'Idris.Core.Value.NDCon', V6, V7, V8, V9, V10}), (('case--reify-4770'('erased', V1, V3, V6, V8, V9, V10, V7, V41, V4, V2, V40, {'Idris.Builtin.MkPair', V40, V10}))(V11)) end end(E32)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3, E4)); _ -> fun (V42) -> ('un--cantReify'('erased', 'erased', V5, <<"List"/utf8>>, V42)) end end.
'dn--un--reflect_Reflect__Visibility'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.Private'} -> (fun () -> fun (V6) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Private"/utf8>>)), V6)) end end()); {'Idris.Core.TT.Export'} -> (fun () -> fun (V7) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Export"/utf8>>)), V7)) end end()); {'Idris.Core.TT.Public'} -> (fun () -> fun (V8) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Public"/utf8>>)), V8)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__TotalReq'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.Total'} -> (fun () -> fun (V6) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Total"/utf8>>)), V6)) end end()); {'Idris.Core.TT.CoveringOnly'} -> (fun () -> fun (V7) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"CoveringOnly"/utf8>>)), V7)) end end()); {'Idris.Core.TT.PartialOK'} -> (fun () -> fun (V8) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"PartialOK"/utf8>>)), V8)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V5, V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PrimVal', V1, {'Idris.Core.TT.Str', V5}}}.
'dn--un--reflect_Reflect__RigCount'(V0, V1, V2, V3, V4, V5) -> ('Idris.Idris2.Algebra.Semiring':'un--elimSemi'('erased', 'erased', {'Idris.Builtin.MkPair', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V6) -> fun (V7) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V6, V7)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V8) -> fun (V9) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V8, V9)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V10) -> fun (V11) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--==_Eq__ZeroOneOmega'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--/=_Eq__ZeroOneOmega'(V12, V13)) end end}}, fun (V14) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"M0"/utf8>>)), V14)) end, fun (V15) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"M1"/utf8>>)), V15)) end, fun (V16) -> fun (V17) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"MW"/utf8>>)), V17)) end end, V5)).
'dn--un--reflect_Reflect__Nat'(V0, V1, V2, V3, V4, V5) -> case V5 of 0 -> fun (V6) -> ('un--getCon'(V0, V1, V2, ('un--preludetypes'(<<"Z"/utf8>>)), V6)) end; _ -> begin (V7 = (V5 - 1)), fun (V8) -> begin (V9 = (('dn--un--reflect_Reflect__Nat'(V0, V1, V2, V3, V4, V7))(V8))), case V9 of {'Idris.Prelude.Types.Left', E0} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V11) -> ('un--appCon'(V0, V1, V2, ('un--preludetypes'(<<"S"/utf8>>)), [V11 | []], V8)) end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end end.
'dn--un--reflect_Reflect__Namespace'(V0, V1, V2, V3, V4, V5, V6) -> begin (V14 = (('dn--un--reflect_Reflect__(List $a)'('erased', fun (V7) -> fun (V8) -> fun (V9) -> fun (V10) -> fun (V11) -> fun (V12) -> fun (V13) -> ('dn--un--reflect_Reflect__String'(V7, V8, V9, V10, V11, V12, V13)) end end end end end end end, V0, V1, V2, V3, V4, ('Idris.Idris2.Core.Name.Namespace':'un--unsafeUnfoldNamespace'(V5))))(V6))), case V14 of {'Idris.Prelude.Types.Left', E0} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V16) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"MkNS"/utf8>>)), [V16 | []], V6)) end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'dn--un--reflect_Reflect__NameType'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.Bound'} -> (fun () -> fun (V6) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Bound"/utf8>>)), V6)) end end()); {'Idris.Core.TT.Func'} -> (fun () -> fun (V7) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Func"/utf8>>)), V7)) end end()); {'Idris.Core.TT.DataCon', E0, E1} -> (fun (V8, V9) -> fun (V10) -> begin (V11 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V8, V10))), case V11 of {'Idris.Prelude.Types.Left', E2} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V13) -> begin (V14 = (('dn--un--reflect_Reflect__Nat'(V0, V1, V2, V3, V4, V9))(V10))), case V14 of {'Idris.Prelude.Types.Left', E4} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V16) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"DataCon"/utf8>>)), [V13 | [V16 | []]], V10)) end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); {'Idris.Core.TT.TyCon', E6, E7} -> (fun (V17, V18) -> fun (V19) -> begin (V20 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V17, V19))), case V20 of {'Idris.Prelude.Types.Left', E8} -> (fun (V21) -> {'Idris.Prelude.Types.Left', V21} end(E8)); {'Idris.Prelude.Types.Right', E9} -> (fun (V22) -> begin (V23 = (('dn--un--reflect_Reflect__Nat'(V0, V1, V2, V3, V4, V18))(V19))), case V23 of {'Idris.Prelude.Types.Left', E10} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V25) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"TyCon"/utf8>>)), [V22 | [V25 | []]], V19)) end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E9)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__Name'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.Name.UN', E0} -> (fun (V6) -> fun (V7) -> begin (V8 = ('dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V6, V7))), case V8 of {'Idris.Prelude.Types.Left', E1} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V10) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"UN"/utf8>>)), [V10 | []], V7)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Core.Name.MN', E3, E4} -> (fun (V11, V12) -> fun (V13) -> begin (V14 = ('dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V11, V13))), case V14 of {'Idris.Prelude.Types.Left', E5} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V16) -> begin (V17 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V12, V13))), case V17 of {'Idris.Prelude.Types.Left', E7} -> (fun (V18) -> {'Idris.Prelude.Types.Left', V18} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V19) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"MN"/utf8>>)), [V16 | [V19 | []]], V13)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E3, E4)); {'Idris.Core.Name.NS', E9, E10} -> (fun (V20, V21) -> fun (V22) -> begin (V23 = ('dn--un--reflect_Reflect__Namespace'(V0, V1, V2, V3, V4, V20, V22))), case V23 of {'Idris.Prelude.Types.Left', E11} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E11)); {'Idris.Prelude.Types.Right', E12} -> (fun (V25) -> begin (V26 = (('dn--un--reflect_Reflect__Name'(V0, V1, V2, V3, V4, V21))(V22))), case V26 of {'Idris.Prelude.Types.Left', E13} -> (fun (V27) -> {'Idris.Prelude.Types.Left', V27} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V28) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"NS"/utf8>>)), [V25 | [V28 | []]], V22)) end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E9, E10)); {'Idris.Core.Name.DN', E15, E16} -> (fun (V29, V30) -> fun (V31) -> begin (V32 = ('dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V29, V31))), case V32 of {'Idris.Prelude.Types.Left', E17} -> (fun (V33) -> {'Idris.Prelude.Types.Left', V33} end(E17)); {'Idris.Prelude.Types.Right', E18} -> (fun (V34) -> begin (V35 = (('dn--un--reflect_Reflect__Name'(V0, V1, V2, V3, V4, V30))(V31))), case V35 of {'Idris.Prelude.Types.Left', E19} -> (fun (V36) -> {'Idris.Prelude.Types.Left', V36} end(E19)); {'Idris.Prelude.Types.Right', E20} -> (fun (V37) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"DN"/utf8>>)), [V34 | [V37 | []]], V31)) end(E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E18)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E15, E16)); {'Idris.Core.Name.Resolved', E21} -> (fun (V38) -> fun (V39) -> begin (V66 = (('Idris.Idris2.Core.Context':'dn--un--full_HasNames__Name'(case V2 of {'Idris.Core.Context.MkDefs', E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47} -> (fun (V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63, V64, V65) -> V40 end(E22, E23, E24, E25, E26, E27, E28, E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.Name.Resolved', V38}))(V39))), case V66 of {'Idris.Prelude.Types.Left', E48} -> (fun (V67) -> {'Idris.Prelude.Types.Left', V67} end(E48)); {'Idris.Prelude.Types.Right', E49} -> (fun (V68) -> case V68 of {'Idris.Core.Name.Resolved', E50} -> (fun (V69) -> ('un--cantReflect'('erased', V1, <<"Name"/utf8>>, V39)) end(E50)); _ -> (('dn--un--reflect_Reflect__Name'(V0, V1, V2, V3, V4, V68))(V39)) end end(E49)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E21)); _ -> fun (V70) -> ('un--cantReflect'('erased', V1, <<"Name"/utf8>>, V70)) end end.
'dn--un--reflect_Reflect__LazyReason'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.LInf'} -> (fun () -> fun (V6) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"LInf"/utf8>>)), V6)) end end()); {'Idris.Core.TT.LLazy'} -> (fun () -> fun (V7) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"LLazy"/utf8>>)), V7)) end end()); {'Idris.Core.TT.LUnknown'} -> (fun () -> fun (V8) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"LUnknown"/utf8>>)), V8)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__Integer'(V0, V1, V2, V3, V4, V5, V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PrimVal', V1, {'Idris.Core.TT.BI', V5}}}.
'dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V5, V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PrimVal', V1, {'Idris.Core.TT.I', V5}}}.
'dn--un--reflect_Reflect__FC'(V0, V1, V2, V3, V4, V5) -> case V3 of 0 -> fun (V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Erased', V1, 1}} end; _ -> case V5 of {'Idris.Core.FC.MkFC', E0, E1, E2} -> (fun (V7, V8, V9) -> fun (V10) -> begin (V11 = ('dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V7, V10))), case V11 of {'Idris.Prelude.Types.Left', E3} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E3)); {'Idris.Prelude.Types.Right', E4} -> (fun (V13) -> begin (V28 = (('dn--un--reflect_Reflect__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', fun (V14) -> fun (V15) -> fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> ('dn--un--reflect_Reflect__Int'(V14, V15, V16, V17, V18, V19, V20)) end end end end end end end, fun (V21) -> fun (V22) -> fun (V23) -> fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> ('dn--un--reflect_Reflect__Int'(V21, V22, V23, V24, V25, V26, V27)) end end end end end end end}, V0, V1, V2, V3, V4, V8))(V10))), case V28 of {'Idris.Prelude.Types.Left', E5} -> (fun (V29) -> {'Idris.Prelude.Types.Left', V29} end(E5)); {'Idris.Prelude.Types.Right', E6} -> (fun (V30) -> begin (V45 = (('dn--un--reflect_Reflect__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', fun (V31) -> fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> fun (V36) -> fun (V37) -> ('dn--un--reflect_Reflect__Int'(V31, V32, V33, V34, V35, V36, V37)) end end end end end end end, fun (V38) -> fun (V39) -> fun (V40) -> fun (V41) -> fun (V42) -> fun (V43) -> fun (V44) -> ('dn--un--reflect_Reflect__Int'(V38, V39, V40, V41, V42, V43, V44)) end end end end end end end}, V0, V1, V2, V3, V4, V9))(V10))), case V45 of {'Idris.Prelude.Types.Left', E7} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V47) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"MkFC"/utf8>>)), [V13 | [V30 | [V47 | []]]], V10)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E6)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E4)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2)); {'Idris.Core.FC.EmptyFC'} -> (fun () -> fun (V48) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"EmptyFC"/utf8>>)), V48)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'dn--un--reflect_Reflect__Double'(V0, V1, V2, V3, V4, V5, V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PrimVal', V1, {'Idris.Core.TT.Db', V5}}}.
'dn--un--reflect_Reflect__Constant'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.I', E0} -> (fun (V6) -> fun (V7) -> begin (V8 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V6, V7))), case V8 of {'Idris.Prelude.Types.Left', E1} -> (fun (V9) -> {'Idris.Prelude.Types.Left', V9} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V10) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"I"/utf8>>)), [V10 | []], V7)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); {'Idris.Core.TT.BI', E3} -> (fun (V11) -> fun (V12) -> begin (V13 = ('dn--un--reflect_Reflect__Integer'(V0, V1, V2, V3, V4, V11, V12))), case V13 of {'Idris.Prelude.Types.Left', E4} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V15) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"BI"/utf8>>)), [V15 | []], V12)) end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E3)); {'Idris.Core.TT.B8', E6} -> (fun (V16) -> fun (V17) -> begin (V18 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V16, V17))), case V18 of {'Idris.Prelude.Types.Left', E7} -> (fun (V19) -> {'Idris.Prelude.Types.Left', V19} end(E7)); {'Idris.Prelude.Types.Right', E8} -> (fun (V20) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"B8"/utf8>>)), [V20 | []], V17)) end(E8)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E6)); {'Idris.Core.TT.B16', E9} -> (fun (V21) -> fun (V22) -> begin (V23 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V21, V22))), case V23 of {'Idris.Prelude.Types.Left', E10} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E10)); {'Idris.Prelude.Types.Right', E11} -> (fun (V25) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"B16"/utf8>>)), [V25 | []], V22)) end(E11)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E9)); {'Idris.Core.TT.B32', E12} -> (fun (V26) -> fun (V27) -> begin (V28 = ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V26, V27))), case V28 of {'Idris.Prelude.Types.Left', E13} -> (fun (V29) -> {'Idris.Prelude.Types.Left', V29} end(E13)); {'Idris.Prelude.Types.Right', E14} -> (fun (V30) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"B32"/utf8>>)), [V30 | []], V27)) end(E14)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E12)); {'Idris.Core.TT.B64', E15} -> (fun (V31) -> fun (V32) -> begin (V33 = ('dn--un--reflect_Reflect__Integer'(V0, V1, V2, V3, V4, V31, V32))), case V33 of {'Idris.Prelude.Types.Left', E16} -> (fun (V34) -> {'Idris.Prelude.Types.Left', V34} end(E16)); {'Idris.Prelude.Types.Right', E17} -> (fun (V35) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"B64"/utf8>>)), [V35 | []], V32)) end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E15)); {'Idris.Core.TT.Str', E18} -> (fun (V36) -> fun (V37) -> begin (V38 = ('dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V36, V37))), case V38 of {'Idris.Prelude.Types.Left', E19} -> (fun (V39) -> {'Idris.Prelude.Types.Left', V39} end(E19)); {'Idris.Prelude.Types.Right', E20} -> (fun (V40) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"Str"/utf8>>)), [V40 | []], V37)) end(E20)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E18)); {'Idris.Core.TT.Ch', E21} -> (fun (V41) -> fun (V42) -> begin (V43 = ('dn--un--reflect_Reflect__Char'(V0, V1, V2, V3, V4, V41, V42))), case V43 of {'Idris.Prelude.Types.Left', E22} -> (fun (V44) -> {'Idris.Prelude.Types.Left', V44} end(E22)); {'Idris.Prelude.Types.Right', E23} -> (fun (V45) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"Ch"/utf8>>)), [V45 | []], V42)) end(E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E21)); {'Idris.Core.TT.Db', E24} -> (fun (V46) -> fun (V47) -> begin (V48 = ('dn--un--reflect_Reflect__Double'(V0, V1, V2, V3, V4, V46, V47))), case V48 of {'Idris.Prelude.Types.Left', E25} -> (fun (V49) -> {'Idris.Prelude.Types.Left', V49} end(E25)); {'Idris.Prelude.Types.Right', E26} -> (fun (V50) -> ('un--appCon'(V0, V1, V2, ('un--reflectiontt'(<<"Db"/utf8>>)), [V50 | []], V47)) end(E26)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E24)); {'Idris.Core.TT.WorldVal'} -> (fun () -> fun (V51) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"WorldVal"/utf8>>)), V51)) end end()); {'Idris.Core.TT.IntType'} -> (fun () -> fun (V52) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"IntType"/utf8>>)), V52)) end end()); {'Idris.Core.TT.IntegerType'} -> (fun () -> fun (V53) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"IntegerType"/utf8>>)), V53)) end end()); {'Idris.Core.TT.Bits8Type'} -> (fun () -> fun (V54) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Bits8Type"/utf8>>)), V54)) end end()); {'Idris.Core.TT.Bits16Type'} -> (fun () -> fun (V55) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Bits16Type"/utf8>>)), V55)) end end()); {'Idris.Core.TT.Bits32Type'} -> (fun () -> fun (V56) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Bits32Type"/utf8>>)), V56)) end end()); {'Idris.Core.TT.Bits64Type'} -> (fun () -> fun (V57) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"Bits64Type"/utf8>>)), V57)) end end()); {'Idris.Core.TT.StringType'} -> (fun () -> fun (V58) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"StringType"/utf8>>)), V58)) end end()); {'Idris.Core.TT.CharType'} -> (fun () -> fun (V59) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"CharType"/utf8>>)), V59)) end end()); {'Idris.Core.TT.DoubleType'} -> (fun () -> fun (V60) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"DoubleType"/utf8>>)), V60)) end end()); {'Idris.Core.TT.WorldType'} -> (fun () -> fun (V61) -> ('un--getCon'(V0, V1, V2, ('un--reflectiontt'(<<"WorldType"/utf8>>)), V61)) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__Char'(V0, V1, V2, V3, V4, V5, V6) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PrimVal', V1, {'Idris.Core.TT.Ch', V5}}}.
'dn--un--reflect_Reflect__Bool'(V0, V1, V2, V3, V4, V5) -> case V5 of 0 -> fun (V6) -> ('un--getCon'(V0, V1, V2, ('un--basics'(<<"True"/utf8>>)), V6)) end; 1 -> fun (V7) -> ('un--getCon'(V0, V1, V2, ('un--basics'(<<"False"/utf8>>)), V7)) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__(|Unit,MkUnit|)'(V0, V1, V2, V3, V4, V5, V6) -> ('un--getCon'(V0, V1, V2, ('un--builtin'(<<"MkUnit"/utf8>>)), V6)).
'dn--un--reflect_Reflect__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of {'Idris.Builtin.MkPair', E0, E1} -> (fun (V9, V10) -> fun (V11) -> begin (V12 = (((((((('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V2))(V3))(V4))(V5))(V6))(V7))(V9))(V11))), case V12 of {'Idris.Prelude.Types.Left', E2} -> (fun (V13) -> {'Idris.Prelude.Types.Left', V13} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V14) -> begin (V15 = (((((((('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V2))(V3))(V4))(V5))(V6))(V7))(V10))(V11))), case V15 of {'Idris.Prelude.Types.Left', E4} -> (fun (V16) -> {'Idris.Prelude.Types.Left', V16} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V17) -> ('un--appCon'(V3, V4, V5, ('un--builtin'(<<"MkPair"/utf8>>)), [{'Idris.Core.TT.Erased', V4, 1} | [{'Idris.Core.TT.Erased', V4, 1} | [V14 | [V17 | []]]]], V11)) end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__(PiInfo $t)'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Core.TT.Implicit'} -> (fun () -> fun (V8) -> ('un--appCon'(V2, V3, V4, ('un--reflectiontt'(<<"ImplicitArg"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | []], V8)) end end()); {'Idris.Core.TT.Explicit'} -> (fun () -> fun (V9) -> ('un--appCon'(V2, V3, V4, ('un--reflectiontt'(<<"ExplicitArg"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | []], V9)) end end()); {'Idris.Core.TT.AutoImplicit'} -> (fun () -> fun (V10) -> ('un--appCon'(V2, V3, V4, ('un--reflectiontt'(<<"AutoImplicit"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | []], V10)) end end()); {'Idris.Core.TT.DefImplicit', E0} -> (fun (V11) -> fun (V12) -> begin (V13 = (((((((V1(V2))(V3))(V4))(V5))(V6))(V11))(V12))), case V13 of {'Idris.Prelude.Types.Left', E1} -> (fun (V14) -> {'Idris.Prelude.Types.Left', V14} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V15) -> ('un--appCon'(V2, V3, V4, ('un--reflectiontt'(<<"DefImplicit"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | [V15 | []]], V12)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__(Maybe $a)'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> fun (V8) -> ('un--appCon'(V2, V3, V4, ('un--preludetypes'(<<"Nothing"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | []], V8)) end end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V9) -> fun (V10) -> begin (V11 = (((((((V1(V2))(V3))(V4))(V5))(V6))(V9))(V10))), case V11 of {'Idris.Prelude.Types.Left', E1} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E1)); {'Idris.Prelude.Types.Right', E2} -> (fun (V13) -> ('un--appCon'(V2, V3, V4, ('un--preludetypes'(<<"Just"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | [V13 | []]], V10)) end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__(List1 $a)'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of {'Idris.Data.List1.:::', E0, E1} -> (fun (V8, V9) -> fun (V10) -> begin (V11 = (((((((V1(V2))(V3))(V4))(V5))(V6))(V8))(V10))), case V11 of {'Idris.Prelude.Types.Left', E2} -> (fun (V12) -> {'Idris.Prelude.Types.Left', V12} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V13) -> begin (V14 = (('dn--un--reflect_Reflect__(List $a)'('erased', V1, V2, V3, V4, V5, V6, V9))(V10))), case V14 of {'Idris.Prelude.Types.Left', E4} -> (fun (V15) -> {'Idris.Prelude.Types.Left', V15} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V16) -> ('un--appCon'(V2, V3, V4, {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--mkNamespace'(<<"Data.List1"/utf8>>)), {'Idris.Core.Name.UN', <<":::"/utf8>>}}, [{'Idris.Core.TT.Erased', V3, 1} | [V13 | [V16 | []]]], V10)) end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--reflect_Reflect__(List $a)'(V0, V1, V2, V3, V4, V5, V6, V7) -> case V7 of [] -> fun (V8) -> ('un--appCon'(V2, V3, V4, ('un--preludetypes'(<<"Nil"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | []], V8)) end; [E0 | E1] -> (fun (V9, V10) -> fun (V11) -> begin (V12 = (((((((V1(V2))(V3))(V4))(V5))(V6))(V9))(V11))), case V12 of {'Idris.Prelude.Types.Left', E2} -> (fun (V13) -> {'Idris.Prelude.Types.Left', V13} end(E2)); {'Idris.Prelude.Types.Right', E3} -> (fun (V14) -> begin (V15 = (('dn--un--reflect_Reflect__(List $a)'('erased', V1, V2, V3, V4, V5, V6, V10))(V11))), case V15 of {'Idris.Prelude.Types.Left', E4} -> (fun (V16) -> {'Idris.Prelude.Types.Left', V16} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V17) -> ('un--appCon'(V2, V3, V4, ('un--preludetypes'(<<"::"/utf8>>)), [{'Idris.Core.TT.Erased', V3, 1} | [V14 | [V17 | []]]], V11)) end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--__Impl_Reify_Visibility'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Visibility'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_TotalReq'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__TotalReq'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_String'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__String'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_RigCount'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__RigCount'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Nat'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Nat'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Namespace'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Namespace'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_NameType'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__NameType'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Name'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Name'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_LazyReason'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__LazyReason'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Integer'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Integer'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Int'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Int'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_FC'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__FC'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Double'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Double'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Constant'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Constant'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Char'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Char'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_Bool'(V0, V1, V2, V3) -> ('dn--un--reify_Reify__Bool'(V0, V1, V2, V3)).
'dn--un--__Impl_Reify_(|Unit,MkUnit|)'(V0, V1, V2, V3, V4) -> ('dn--un--reify_Reify__(|Unit,MkUnit|)'(V0, V1, V2, V3, V4)).
'dn--un--__Impl_Reify_(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reify_Reify__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reify_(PiInfo $t)'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reify_Reify__(PiInfo $t)'('erased', V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reify_(Maybe $a)'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reify_Reify__(Maybe $a)'('erased', V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reify_(List1 $a)'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reify_Reify__(List1 $a)'('erased', V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reify_(List $a)'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reify_Reify__(List $a)'('erased', V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Visibility'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__Visibility'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_TotalReq'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__TotalReq'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_String'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reflect_Reflect__String'(V0, V1, V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reflect_RigCount'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__RigCount'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Nat'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__Nat'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Namespace'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reflect_Reflect__Namespace'(V0, V1, V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reflect_NameType'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__NameType'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Name'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__Name'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_LazyReason'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__LazyReason'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Integer'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reflect_Reflect__Integer'(V0, V1, V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reflect_Int'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reflect_Reflect__Int'(V0, V1, V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reflect_FC'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__FC'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Double'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reflect_Reflect__Double'(V0, V1, V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reflect_Constant'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__Constant'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_Char'(V0, V1, V2, V3, V4, V5, V6) -> ('dn--un--reflect_Reflect__Char'(V0, V1, V2, V3, V4, V5, V6)).
'dn--un--__Impl_Reflect_Bool'(V0, V1, V2, V3, V4, V5) -> ('dn--un--reflect_Reflect__Bool'(V0, V1, V2, V3, V4, V5)).
'dn--un--__Impl_Reflect_(|Unit,MkUnit|)'(V0, V1, V2, V3, V4, V5) -> fun (V6) -> ('dn--un--reflect_Reflect__(|Unit,MkUnit|)'(V0, V1, V2, V3, V4, V5, V6)) end.
'dn--un--__Impl_Reflect_(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> ('dn--un--reflect_Reflect__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', V2, V3, V4, V5, V6, V7, V8)).
'dn--un--__Impl_Reflect_(PiInfo $t)'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('dn--un--reflect_Reflect__(PiInfo $t)'('erased', V1, V2, V3, V4, V5, V6, V7)).
'dn--un--__Impl_Reflect_(Maybe $a)'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('dn--un--reflect_Reflect__(Maybe $a)'('erased', V1, V2, V3, V4, V5, V6, V7)).
'dn--un--__Impl_Reflect_(List1 $a)'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('dn--un--reflect_Reflect__(List1 $a)'('erased', V1, V2, V3, V4, V5, V6, V7)).
'dn--un--__Impl_Reflect_(List $a)'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('dn--un--reflect_Reflect__(List $a)'('erased', V1, V2, V3, V4, V5, V6, V7)).
'un--reify'(V0, V1, V2, V3, V4, V5) -> ((((V3(V1))(V2))(V4))(V5)).
'un--reflectionttimp'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--reflectionTTImpNS'()), {'Idris.Core.Name.UN', V0}}.
'un--reflectiontt'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--reflectionTTNS'()), {'Idris.Core.Name.UN', V0}}.
'un--reflection'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--reflectionNS'()), {'Idris.Core.Name.UN', V0}}.
'un--reflect'(V0, V1, V2, V3, V4, V5, V6, V7) -> ((((((V2(V1))(V3))(V4))(V5))(V6))(V7)).
'un--primio'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--primIONS'()), {'Idris.Core.Name.UN', V0}}.
'un--preludetypes'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--typesNS'()), {'Idris.Core.Name.UN', V0}}.
'un--getCon'(V0, V1, V2, V3, V4) -> begin (V31 = ('Idris.Idris2.Core.Context':'un--lookupDefExact'(V3, case V2 of {'Idris.Core.Context.MkDefs', E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25} -> (fun (V5, V6, V7, V8, V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30) -> V5 end(E0, E1, E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, V4))), case V31 of {'Idris.Prelude.Types.Left', E26} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E26)); {'Idris.Prelude.Types.Right', E27} -> (fun (V33) -> case V33 of {'Idris.Prelude.Types.Just', E28} -> (fun (V34) -> case V34 of {'Idris.Core.Context.DCon', E55, E56, E57} -> (fun (V35, V36, V37) -> (('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81, E82, E83} -> (fun (V38, V39, V40, V41, V42, V43, V44, V45, V46, V47, V48, V49, V50, V51, V52, V53, V54, V55, V56, V57, V58, V59, V60, V61, V62, V63) -> V38 end(E58, E59, E60, E61, E62, E63, E64, E65, E66, E67, E68, E69, E70, E71, E72, E73, E74, E75, E76, E77, E78, E79, E80, E81, E82, E83)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.TT.Ref', V1, {'Idris.Core.TT.DataCon', V35, V36}, V3}))(V4)) end(E55, E56, E57)); {'Idris.Core.Context.TCon', E84, E85, E86, E87, E88, E89, E90, E91} -> (fun (V64, V65, V66, V67, V68, V69, V70, V71) -> (('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E92, E93, E94, E95, E96, E97, E98, E99, E100, E101, E102, E103, E104, E105, E106, E107, E108, E109, E110, E111, E112, E113, E114, E115, E116, E117} -> (fun (V72, V73, V74, V75, V76, V77, V78, V79, V80, V81, V82, V83, V84, V85, V86, V87, V88, V89, V90, V91, V92, V93, V94, V95, V96, V97) -> V72 end(E92, E93, E94, E95, E96, E97, E98, E99, E100, E101, E102, E103, E104, E105, E106, E107, E108, E109, E110, E111, E112, E113, E114, E115, E116, E117)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.TT.Ref', V1, {'Idris.Core.TT.TyCon', V64, V65}, V3}))(V4)) end(E84, E85, E86, E87, E88, E89, E90, E91)); _ -> (('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54} -> (fun (V98, V99, V100, V101, V102, V103, V104, V105, V106, V107, V108, V109, V110, V111, V112, V113, V114, V115, V116, V117, V118, V119, V120, V121, V122, V123) -> V98 end(E29, E30, E31, E32, E33, E34, E35, E36, E37, E38, E39, E40, E41, E42, E43, E44, E45, E46, E47, E48, E49, E50, E51, E52, E53, E54)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, {'Idris.Core.TT.Ref', V1, {'Idris.Core.TT.Func'}, V3}))(V4)) end end(E28)); _ -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.UndefinedName', V1, V3}, V4)) end end(E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--cantReify'(V0, V1, V2, V3, V4) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', ('Idris.Idris2.Core.Value':'un--getLoc'('erased', V2)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Can\x{27}t reify as "/utf8>>, V3))}, V4)).
'un--cantReflect'(V0, V1, V2, V3) -> ('Idris.Idris2.Core.Core':'dn--un--throw_Catchable__Core_Error'('erased', {'Idris.Core.Core.GenericMsg', V1, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"Can\x{27}t reflect as "/utf8>>, V2))}, V3)).
'un--builtin'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--builtinNS'()), {'Idris.Core.Name.UN', V0}}.
'un--basics'(V0) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--basicsNS'()), {'Idris.Core.Name.UN', V0}}.
'un--appCon'(V0, V1, V2, V3, V4, V5) -> begin (V6 = ('un--getCon'(V0, V1, V2, V3, V5))), case V6 of {'Idris.Prelude.Types.Left', E0} -> (fun (V7) -> {'Idris.Prelude.Types.Left', V7} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V8) -> (('Idris.Idris2.Core.Context':'dn--un--resolved_HasNames__(Term $vars)'('erased', case V2 of {'Idris.Core.Context.MkDefs', E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27} -> (fun (V9, V10, V11, V12, V13, V14, V15, V16, V17, V18, V19, V20, V21, V22, V23, V24, V25, V26, V27, V28, V29, V30, V31, V32, V33, V34) -> V9 end(E2, E3, E4, E5, E6, E7, E8, E9, E10, E11, E12, E13, E14, E15, E16, E17, E18, E19, E20, E21, E22, E23, E24, E25, E26, E27)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end, ('Idris.Idris2.Core.TT':'un--apply'('erased', V1, V8, V4))))(V5)) end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.