Packages

Erlang code generator for Idris 2

Current section

Files

Jump to
idris2 src Idris.Idris2.Core.Name.erl
Raw

src/Idris.Idris2.Core.Name.erl

-module('Idris.Idris2.Core.Name').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
'with--nameEq-8965'/3,
'with--with block in nameEq-8938'/4,
'with--nameEq-8917'/5,
'with--with block in nameEq-8890'/4,
'with--nameEq-8869'/5,
'with--with block in nameEq-8849'/4,
'with--nameEq-8825'/5,
'with--with block in nameEq-8792'/4,
'with--nameEq-8781'/5,
'with--with block in nameEq-8751'/4,
'with--nameEq-8740'/5,
'with--with block in nameEq-8711'/4,
'with--nameEq-8696'/5,
'with--nameEq-8669'/3,
'with--with block in nameEq-8643'/4,
'with--nameEq-8632'/5,
'case--compare-8569'/5,
'case--compare-8529'/5,
'case--compare-8485'/5,
'case--compare-8435'/5,
'case--compare-8395'/5,
'case--compare-8349'/5,
'case--max-8310'/3,
'case--min-8296'/3,
'dn--un--show_Show__Name'/1,
'dn--un--showPrec_Show__Name'/2,
'dn--un--pretty_Pretty__Name'/2,
'dn--un--prettyPrec_Pretty__Name'/3,
'dn--un--min_Ord__Name'/2,
'dn--un--max_Ord__Name'/2,
'dn--un--compare_Ord__Name'/2,
'dn--un--__Impl_Show_Name'/0,
'dn--un--__Impl_Pretty_Name'/0,
'dn--un--__Impl_Ord_Name'/0,
'dn--un--__Impl_Eq_Name'/0,
'dn--un-->_Ord__Name'/2,
'dn--un-->=_Ord__Name'/2,
'dn--un--==_Eq__Name'/2,
'dn--un--<_Ord__Name'/2,
'dn--un--<=_Ord__Name'/2,
'dn--un--/=_Eq__Name'/2,
'un--userNameRoot'/1,
'un--namesEq'/2,
'un--nameTag'/1,
'un--nameRoot'/1,
'un--nameEq'/2,
'un--mkNamespacedName'/2,
'un--matches'/2,
'un--isUserName'/1,
'un--dropNS'/1,
'un--dropAllNS'/1,
'un--asName'/3
]).
'with--nameEq-8965'(V0, V1, V2) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V3) -> case V3 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V4) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8938'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.No', E0} -> (fun (V4) -> {'Idris.Prelude.Types.Nothing'} end(E0)); {'Idris.Prelude.Types.Yes', E1} -> (fun (V5) -> case V5 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8917'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.No', E0} -> (fun (V5) -> {'Idris.Prelude.Types.Nothing'} end(E0)); {'Idris.Prelude.Types.Yes', E1} -> (fun (V6) -> case V6 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8938'(V4, V3, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8890'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.No', E0} -> (fun (V4) -> {'Idris.Prelude.Types.Nothing'} end(E0)); {'Idris.Prelude.Types.Yes', E1} -> (fun (V5) -> case V5 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8869'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.No', E0} -> (fun (V5) -> {'Idris.Prelude.Types.Nothing'} end(E0)); {'Idris.Prelude.Types.Yes', E1} -> (fun (V6) -> case V6 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8890'(V4, V3, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8849'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Nothing'} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> case V4 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8825'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.No', E0} -> (fun (V5) -> {'Idris.Prelude.Types.Nothing'} end(E0)); {'Idris.Prelude.Types.Yes', E1} -> (fun (V6) -> case V6 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8849'(V4, V3, ('un--nameEq'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8792'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> case V4 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Nothing'} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8781'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V5) -> case V5 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8792'(V4, V3, ('un--nameEq'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V6) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8751'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V4) -> case V4 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V5) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8740'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.Just', E0} -> (fun (V5) -> case V5 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8751'(V4, V3, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Nothing'} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8711'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V4) -> case V4 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V5) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8696'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V5) -> case V5 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8711'(V4, V3, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V6) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8669'(V0, V1, V2) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V3) -> case V3 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V4) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--with block in nameEq-8643'(V0, V1, V2, V3) -> case V2 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Prelude.Types.Nothing'} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V4) -> case V4 of {'Idris.Builtin.Refl'} -> (fun () -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'with--nameEq-8632'(V0, V1, V2, V3, V4) -> case V2 of {'Idris.Prelude.Types.Yes', E0} -> (fun (V5) -> case V5 of {'Idris.Builtin.Refl'} -> (fun () -> ('with--with block in nameEq-8643'(V4, V3, ('un--nameEq'(V3, V4)), V0)) end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0)); {'Idris.Prelude.Types.No', E1} -> (fun (V6) -> {'Idris.Prelude.Types.Nothing'} end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--compare-8569'(V0, V1, V2, V3, V4) -> case V4 of 1 -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__String'(V1, V3)); 2 -> 2; 0 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--compare-8529'(V0, V1, V2, V3, V4) -> case V4 of 1 -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__String'(V1, V3)); 2 -> 2; 0 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--compare-8485'(V0, V1, V2, V3, V4) -> case V4 of 1 -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V5) -> fun (V6) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V5, V6)) end end, fun (V7) -> fun (V8) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Int'(V7, V8)) end end}, fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V11, V12)) end end, fun (V13) -> fun (V14) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->_Ord__Int'(V13, V14)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<=_Ord__Int'(V15, V16)) end end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->=_Ord__Int'(V17, V18)) end end, fun (V19) -> fun (V20) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--max_Ord__Int'(V19, V20)) end end, fun (V21) -> fun (V22) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--min_Ord__Int'(V21, V22)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V23) -> fun (V24) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V23, V24)) end end, fun (V25) -> fun (V26) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Int'(V25, V26)) end end}, fun (V27) -> fun (V28) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V27, V28)) end end, fun (V29) -> fun (V30) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V29, V30)) end end, fun (V31) -> fun (V32) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->_Ord__Int'(V31, V32)) end end, fun (V33) -> fun (V34) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--<=_Ord__Int'(V33, V34)) end end, fun (V35) -> fun (V36) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un-->=_Ord__Int'(V35, V36)) end end, fun (V37) -> fun (V38) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--max_Ord__Int'(V37, V38)) end end, fun (V39) -> fun (V40) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--min_Ord__Int'(V39, V40)) end end}, V1, V3)); 2 -> 2; 0 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--compare-8435'(V0, V1, V2, V3, V4) -> case V4 of 1 -> ('dn--un--compare_Ord__Name'(V1, V3)); 2 -> 2; 0 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--compare-8395'(V0, V1, V2, V3, V4) -> case V4 of 1 -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__String'(V1, V3)); 2 -> 2; 0 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--compare-8349'(V0, V1, V2, V3, V4) -> case V4 of 1 -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--compare_Ord__Namespace'(V1, V3)); 2 -> 2; 0 -> 0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--max-8310'(V0, V1, V2) -> case V2 of 0 -> V1; 1 -> V0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--min-8296'(V0, V1, V2) -> case V2 of 0 -> V1; 1 -> V0; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--show_Show__Name'(V0) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V1, V2) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Core.Name.Namespace':'dn--un--show_Show__Namespace'(V1)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"."/utf8>>, ('dn--un--show_Show__Name'(V2)))))) end(E0, E1)); {'Idris.Core.Name.UN', E2} -> (fun (V3) -> V3 end(E2)); {'Idris.Core.Name.MN', E3, E4} -> (fun (V4, V5) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"{"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(V4, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<":"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V5)), <<"}"/utf8>>)))))))) end(E3, E4)); {'Idris.Core.Name.PV', E5, E6} -> (fun (V6, V7) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"{P:"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('dn--un--show_Show__Name'(V6)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<":"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V7)), <<"}"/utf8>>)))))))) end(E5, E6)); {'Idris.Core.Name.DN', E7, E8} -> (fun (V8, V9) -> V8 end(E7, E8)); {'Idris.Core.Name.Nested', E9, E10} -> (fun (V10, V11) -> case V10 of {'Idris.Builtin.MkPair', E11, E12} -> (fun (V12, V13) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V12)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<":"/utf8>>, ('Idris.Idris2.Prelude.Types.Strings':'un--++'(('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V13)), ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<":"/utf8>>, ('dn--un--show_Show__Name'(V11)))))))))) end(E11, E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E9, E10)); {'Idris.Core.Name.CaseBlock', E13, E14} -> (fun (V14, V15) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"case block in "/utf8>>, V14)) end(E13, E14)); {'Idris.Core.Name.WithBlock', E15, E16} -> (fun (V16, V17) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"with block in "/utf8>>, V16)) end(E15, E16)); {'Idris.Core.Name.Resolved', E17} -> (fun (V18) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"$resolved"/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V18)))) end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--showPrec_Show__Name'(V0, V1) -> ('dn--un--show_Show__Name'(V1)).
'dn--un--pretty_Pretty__Name'(V0, V1) -> case V1 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V2, V3) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Core.Name.Namespace':'dn--un--pretty_Pretty__Namespace'('erased', V2)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--dot'('erased')))), ('dn--un--pretty_Pretty__Name'('erased', V3)))) end(E0, E1)); {'Idris.Core.Name.UN', E2} -> (fun (V4) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', V4)) end(E2)); {'Idris.Core.Name.MN', E3, E4} -> (fun (V5, V6) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--braces'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', V5)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--colon'('erased')))), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__Int'('erased', V6)))))) end(E3, E4)); {'Idris.Core.Name.PV', E5, E6} -> (fun (V7, V8) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--braces'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__Char'('erased', $P)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--colon'('erased')))), ('dn--un--pretty_Pretty__Name'('erased', V7)))), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--colon'('erased')))), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__Int'('erased', V8)))))) end(E5, E6)); {'Idris.Core.Name.DN', E7, E8} -> (fun (V9, V10) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', V9)) end(E7, E8)); {'Idris.Core.Name.Nested', E9, E10} -> (fun (V11, V12) -> case V11 of {'Idris.Builtin.MkPair', E11, E12} -> (fun (V13, V14) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__Int'('erased', V13)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--colon'('erased')))), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__Int'('erased', V14)))), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Symbols':'un--colon'('erased')))), ('dn--un--pretty_Pretty__Name'('erased', V12)))) end(E11, E12)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E9, E10)); {'Idris.Core.Name.CaseBlock', E13, E14} -> (fun (V15, V16) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Util':'un--reflow'('erased', <<"case block in"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', V15)))) end(E13, E14)); {'Idris.Core.Name.WithBlock', E15, E16} -> (fun (V17, V18) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'un--<++>'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Util':'un--reflow'('erased', <<"with block in"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', V17)))) end(E15, E16)); {'Idris.Core.Name.Resolved', E17} -> (fun (V19) -> ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--<+>_Semigroup__(Doc $ann)'('erased', ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__String'('erased', <<"$resolved"/utf8>>)), ('Idris.Idris2.Text.PrettyPrint.Prettyprinter.Doc':'dn--un--pretty_Pretty__Int'('erased', V19)))) end(E17)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'dn--un--prettyPrec_Pretty__Name'(V0, V1, V2) -> ('dn--un--pretty_Pretty__Name'('erased', V2)).
'dn--un--min_Ord__Name'(V0, V1) -> ('case--min-8296'(V1, V0, ('dn--un--<_Ord__Name'(V0, V1)))).
'dn--un--max_Ord__Name'(V0, V1) -> ('case--max-8310'(V1, V0, ('dn--un-->_Ord__Name'(V0, V1)))).
'dn--un--compare_Ord__Name'(V0, V1) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V2, V3) -> case V1 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V4, V5) -> ('case--compare-8349'(V3, V2, V5, V4, ('dn--un--compare_Ord__Name'(V3, V5)))) end(E2, E3)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E0, E1)); {'Idris.Core.Name.UN', E4} -> (fun (V6) -> case V1 of {'Idris.Core.Name.UN', E5} -> (fun (V7) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__String'(V6, V7)) end(E5)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E4)); {'Idris.Core.Name.MN', E6, E7} -> (fun (V8, V9) -> case V1 of {'Idris.Core.Name.MN', E8, E9} -> (fun (V10, V11) -> ('case--compare-8395'(V9, V8, V11, V10, ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V9, V11)))) end(E8, E9)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E6, E7)); {'Idris.Core.Name.PV', E10, E11} -> (fun (V12, V13) -> case V1 of {'Idris.Core.Name.PV', E12, E13} -> (fun (V14, V15) -> ('case--compare-8435'(V13, V12, V15, V14, ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V13, V15)))) end(E12, E13)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E10, E11)); {'Idris.Core.Name.DN', E14, E15} -> (fun (V16, V17) -> case V1 of {'Idris.Core.Name.DN', E16, E17} -> (fun (V18, V19) -> ('dn--un--compare_Ord__Name'(V17, V19)) end(E16, E17)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E14, E15)); {'Idris.Core.Name.Nested', E18, E19} -> (fun (V20, V21) -> case V1 of {'Idris.Core.Name.Nested', E20, E21} -> (fun (V22, V23) -> ('case--compare-8485'(V21, V20, V23, V22, ('dn--un--compare_Ord__Name'(V21, V23)))) end(E20, E21)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E18, E19)); {'Idris.Core.Name.CaseBlock', E22, E23} -> (fun (V24, V25) -> case V1 of {'Idris.Core.Name.CaseBlock', E24, E25} -> (fun (V26, V27) -> ('case--compare-8529'(V25, V24, V27, V26, ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V25, V27)))) end(E24, E25)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E22, E23)); {'Idris.Core.Name.WithBlock', E26, E27} -> (fun (V28, V29) -> case V1 of {'Idris.Core.Name.WithBlock', E28, E29} -> (fun (V30, V31) -> ('case--compare-8569'(V29, V28, V31, V30, ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V29, V31)))) end(E28, E29)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E26, E27)); {'Idris.Core.Name.Resolved', E30} -> (fun (V32) -> case V1 of {'Idris.Core.Name.Resolved', E31} -> (fun (V33) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(V32, V33)) end(E31)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end end(E30)); _ -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--compare_Ord__Int'(('un--nameTag'(V0)), ('un--nameTag'(V1)))) end.
'dn--un--__Impl_Show_Name'() -> {'Idris.Prelude.Show.dn--un--__mkShow', fun (V0) -> ('dn--un--show_Show__Name'(V0)) end, fun (V1) -> fun (V2) -> ('dn--un--showPrec_Show__Name'(V1, V2)) end end}.
'dn--un--__Impl_Pretty_Name'() -> {'Idris.Text.PrettyPrint.Prettyprinter.Doc.dn--un--__mkPretty', fun (V0) -> fun (V1) -> ('dn--un--pretty_Pretty__Name'('erased', V1)) end end, fun (V2) -> fun (V3) -> fun (V4) -> ('dn--un--prettyPrec_Pretty__Name'('erased', V3, V4)) end end end}.
'dn--un--__Impl_Ord_Name'() -> {'Idris.Prelude.EqOrd.dn--un--__mkOrd', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V0) -> fun (V1) -> ('dn--un--==_Eq__Name'(V0, V1)) end end, fun (V2) -> fun (V3) -> ('dn--un--/=_Eq__Name'(V2, V3)) end end}, fun (V4) -> fun (V5) -> ('dn--un--compare_Ord__Name'(V4, V5)) end end, fun (V6) -> fun (V7) -> ('dn--un--<_Ord__Name'(V6, V7)) end end, fun (V8) -> fun (V9) -> ('dn--un-->_Ord__Name'(V8, V9)) end end, fun (V10) -> fun (V11) -> ('dn--un--<=_Ord__Name'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('dn--un-->=_Ord__Name'(V12, V13)) end end, fun (V14) -> fun (V15) -> ('dn--un--max_Ord__Name'(V14, V15)) end end, fun (V16) -> fun (V17) -> ('dn--un--min_Ord__Name'(V16, V17)) end end}.
'dn--un--__Impl_Eq_Name'() -> {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V0) -> fun (V1) -> ('dn--un--==_Eq__Name'(V0, V1)) end end, fun (V2) -> fun (V3) -> ('dn--un--/=_Eq__Name'(V2, V3)) end end}.
'dn--un-->_Ord__Name'(V0, V1) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Ordering'(('dn--un--compare_Ord__Name'(V0, V1)), 2)).
'dn--un-->=_Ord__Name'(V0, V1) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Ordering'(('dn--un--compare_Ord__Name'(V0, V1)), 0)).
'dn--un--==_Eq__Name'(V0, V1) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V2, V3) -> case V1 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V4, V5) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('dn--un--==_Eq__Name'(V3, V5)), fun () -> ('Idris.Idris2.Core.Name.Namespace':'dn--un--==_Eq__Namespace'(V2, V4)) end)) end(E2, E3)); _ -> 1 end end(E0, E1)); {'Idris.Core.Name.UN', E4} -> (fun (V6) -> case V1 of {'Idris.Core.Name.UN', E5} -> (fun (V7) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V6, V7)) end(E5)); _ -> 1 end end(E4)); {'Idris.Core.Name.MN', E6, E7} -> (fun (V8, V9) -> case V1 of {'Idris.Core.Name.MN', E8, E9} -> (fun (V10, V11) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V9, V11)), fun () -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V8, V10)) end)) end(E8, E9)); _ -> 1 end end(E6, E7)); {'Idris.Core.Name.PV', E10, E11} -> (fun (V12, V13) -> case V1 of {'Idris.Core.Name.PV', E12, E13} -> (fun (V14, V15) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('dn--un--==_Eq__Name'(V12, V14)), fun () -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V13, V15)) end)) end(E12, E13)); _ -> 1 end end(E10, E11)); {'Idris.Core.Name.DN', E14, E15} -> (fun (V16, V17) -> case V1 of {'Idris.Core.Name.DN', E16, E17} -> (fun (V18, V19) -> ('dn--un--==_Eq__Name'(V17, V19)) end(E16, E17)); _ -> 1 end end(E14, E15)); {'Idris.Core.Name.Nested', E18, E19} -> (fun (V20, V21) -> case V1 of {'Idris.Core.Name.Nested', E20, E21} -> (fun (V22, V23) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V24) -> fun (V25) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V24, V25)) end end, fun (V26) -> fun (V27) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Int'(V26, V27)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V28) -> fun (V29) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V28, V29)) end end, fun (V30) -> fun (V31) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Int'(V30, V31)) end end}, V20, V22)), fun () -> ('dn--un--==_Eq__Name'(V21, V23)) end)) end(E20, E21)); _ -> 1 end end(E18, E19)); {'Idris.Core.Name.CaseBlock', E22, E23} -> (fun (V32, V33) -> case V1 of {'Idris.Core.Name.CaseBlock', E24, E25} -> (fun (V34, V35) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V33, V35)), fun () -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V32, V34)) end)) end(E24, E25)); _ -> 1 end end(E22, E23)); {'Idris.Core.Name.WithBlock', E26, E27} -> (fun (V36, V37) -> case V1 of {'Idris.Core.Name.WithBlock', E28, E29} -> (fun (V38, V39) -> ('Idris.Idris2.Prelude.Basics':'un--&&'(('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V37, V39)), fun () -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V36, V38)) end)) end(E28, E29)); _ -> 1 end end(E26, E27)); {'Idris.Core.Name.Resolved', E30} -> (fun (V40) -> case V1 of {'Idris.Core.Name.Resolved', E31} -> (fun (V41) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(V40, V41)) end(E31)); _ -> 1 end end(E30)); _ -> 1 end.
'dn--un--<_Ord__Name'(V0, V1) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Ordering'(('dn--un--compare_Ord__Name'(V0, V1)), 0)).
'dn--un--<=_Ord__Name'(V0, V1) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__Ordering'(('dn--un--compare_Ord__Name'(V0, V1)), 2)).
'dn--un--/=_Eq__Name'(V0, V1) -> ('Idris.Idris2.Prelude.Basics':'un--not'(('dn--un--==_Eq__Name'(V0, V1)))).
'un--userNameRoot'(V0) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V1, V2) -> ('un--userNameRoot'(V2)) end(E0, E1)); {'Idris.Core.Name.UN', E2} -> (fun (V3) -> {'Idris.Prelude.Types.Just', V3} end(E2)); {'Idris.Core.Name.DN', E3, E4} -> (fun (V4, V5) -> ('un--userNameRoot'(V5)) end(E3, E4)); _ -> {'Idris.Prelude.Types.Nothing'} end.
'un--namesEq'(V0, V1) -> case V0 of [] -> case V1 of [] -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}}; _ -> {'Idris.Prelude.Types.Nothing'} end; [E0 | E1] -> (fun (V2, V3) -> case V1 of [E2 | E3] -> (fun (V4, V5) -> ('Idris.Idris2.Prelude.Types':'dn--un-->>=_Monad__Maybe'('erased', 'erased', ('un--nameEq'(V2, V4)), fun (V6) -> ('Idris.Idris2.Prelude.Types':'dn--un-->>=_Monad__Maybe'('erased', 'erased', ('un--namesEq'(V3, V5)), fun (V7) -> {'Idris.Prelude.Types.Just', {'Idris.Builtin.Refl'}} end)) end)) end(E2, E3)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E0, E1)); _ -> {'Idris.Prelude.Types.Nothing'} end.
'un--nameTag'(V0) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V1, V2) -> 0 end(E0, E1)); {'Idris.Core.Name.UN', E2} -> (fun (V3) -> 1 end(E2)); {'Idris.Core.Name.MN', E3, E4} -> (fun (V4, V5) -> 2 end(E3, E4)); {'Idris.Core.Name.PV', E5, E6} -> (fun (V6, V7) -> 3 end(E5, E6)); {'Idris.Core.Name.DN', E7, E8} -> (fun (V8, V9) -> 4 end(E7, E8)); {'Idris.Core.Name.Nested', E9, E10} -> (fun (V10, V11) -> 5 end(E9, E10)); {'Idris.Core.Name.CaseBlock', E11, E12} -> (fun (V12, V13) -> 6 end(E11, E12)); {'Idris.Core.Name.WithBlock', E13, E14} -> (fun (V14, V15) -> 7 end(E13, E14)); {'Idris.Core.Name.Resolved', E15} -> (fun (V16) -> 8 end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--nameRoot'(V0) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V1, V2) -> ('un--nameRoot'(V2)) end(E0, E1)); {'Idris.Core.Name.UN', E2} -> (fun (V3) -> V3 end(E2)); {'Idris.Core.Name.MN', E3, E4} -> (fun (V4, V5) -> V4 end(E3, E4)); {'Idris.Core.Name.PV', E5, E6} -> (fun (V6, V7) -> ('un--nameRoot'(V6)) end(E5, E6)); {'Idris.Core.Name.DN', E7, E8} -> (fun (V8, V9) -> ('un--nameRoot'(V9)) end(E7, E8)); {'Idris.Core.Name.Nested', E9, E10} -> (fun (V10, V11) -> ('un--nameRoot'(V11)) end(E9, E10)); {'Idris.Core.Name.CaseBlock', E11, E12} -> (fun (V12, V13) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"$"/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V12)))) end(E11, E12)); {'Idris.Core.Name.WithBlock', E13, E14} -> (fun (V14, V15) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"$"/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__String'(V14)))) end(E13, E14)); {'Idris.Core.Name.Resolved', E15} -> (fun (V16) -> ('Idris.Idris2.Prelude.Types.Strings':'un--++'(<<"$"/utf8>>, ('Idris.Idris2.Prelude.Show':'dn--un--show_Show__Int'(V16)))) end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--nameEq'(V0, V1) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V2, V3) -> case V1 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V4, V5) -> ('with--nameEq-8632'(V2, V4, ('Idris.Idris2.Core.Name.Namespace':'dn--un--decEq_DecEq__Namespace'(V2, V4)), V3, V5)) end(E2, E3)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E0, E1)); {'Idris.Core.Name.UN', E4} -> (fun (V6) -> case V1 of {'Idris.Core.Name.UN', E5} -> (fun (V7) -> ('with--nameEq-8669'(V6, V7, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__String'(V6, V7)))) end(E5)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E4)); {'Idris.Core.Name.MN', E6, E7} -> (fun (V8, V9) -> case V1 of {'Idris.Core.Name.MN', E8, E9} -> (fun (V10, V11) -> ('with--nameEq-8696'(V8, V10, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__String'(V8, V10)), V9, V11)) end(E8, E9)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E6, E7)); {'Idris.Core.Name.PV', E10, E11} -> (fun (V12, V13) -> case V1 of {'Idris.Core.Name.PV', E12, E13} -> (fun (V14, V15) -> ('with--nameEq-8740'(V12, V14, ('un--nameEq'(V12, V14)), V13, V15)) end(E12, E13)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E10, E11)); {'Idris.Core.Name.DN', E14, E15} -> (fun (V16, V17) -> case V1 of {'Idris.Core.Name.DN', E16, E17} -> (fun (V18, V19) -> ('with--nameEq-8781'(V16, V18, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__String'(V16, V18)), V17, V19)) end(E16, E17)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E14, E15)); {'Idris.Core.Name.Nested', E18, E19} -> (fun (V20, V21) -> case V1 of {'Idris.Core.Name.Nested', E20, E21} -> (fun (V22, V23) -> ('with--nameEq-8825'(V20, V22, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Builtin.MkPair', fun (V24) -> fun (V25) -> ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V24, V25)) end end, fun (V26) -> fun (V27) -> ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V26, V27)) end end}, V20, V22)), V21, V23)) end(E20, E21)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E18, E19)); {'Idris.Core.Name.CaseBlock', E22, E23} -> (fun (V28, V29) -> case V1 of {'Idris.Core.Name.CaseBlock', E24, E25} -> (fun (V30, V31) -> ('with--nameEq-8869'(V28, V30, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__String'(V28, V30)), V29, V31)) end(E24, E25)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E22, E23)); {'Idris.Core.Name.WithBlock', E26, E27} -> (fun (V32, V33) -> case V1 of {'Idris.Core.Name.WithBlock', E28, E29} -> (fun (V34, V35) -> ('with--nameEq-8917'(V32, V34, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__String'(V32, V34)), V33, V35)) end(E28, E29)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E26, E27)); {'Idris.Core.Name.Resolved', E30} -> (fun (V36) -> case V1 of {'Idris.Core.Name.Resolved', E31} -> (fun (V37) -> ('with--nameEq-8965'(V36, V37, ('Idris.Idris2.Decidable.Equality':'dn--un--decEq_DecEq__Int'(V36, V37)))) end(E31)); _ -> {'Idris.Prelude.Types.Nothing'} end end(E30)); _ -> {'Idris.Prelude.Types.Nothing'} end.
'un--mkNamespacedName'(V0, V1) -> case V0 of {'Idris.Prelude.Types.Nothing'} -> (fun () -> {'Idris.Core.Name.UN', V1} end()); {'Idris.Prelude.Types.Just', E0} -> (fun (V2) -> {'Idris.Core.Name.NS', V2, {'Idris.Core.Name.UN', V1}} end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--matches'(V0, V1) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V2, V3) -> case V1 of {'Idris.Core.Name.NS', E2, E3} -> (fun (V4, V5) -> ('Idris.Idris2.Core.Name.Namespace':'un--isApproximationOf'(V2, V4)) end(E2, E3)); _ -> 0 end end(E0, E1)); _ -> 0 end.
'un--isUserName'(V0) -> case V0 of {'Idris.Core.Name.PV', E0, E1} -> (fun (V1, V2) -> 1 end(E0, E1)); {'Idris.Core.Name.MN', E2, E3} -> (fun (V3, V4) -> 1 end(E2, E3)); {'Idris.Core.Name.NS', E4, E5} -> (fun (V5, V6) -> ('un--isUserName'(V6)) end(E4, E5)); {'Idris.Core.Name.DN', E6, E7} -> (fun (V7, V8) -> ('un--isUserName'(V8)) end(E6, E7)); _ -> 0 end.
'un--dropNS'(V0) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V1, V2) -> V2 end(E0, E1)); _ -> V0 end.
'un--dropAllNS'(V0) -> case V0 of {'Idris.Core.Name.NS', E0, E1} -> (fun (V1, V2) -> ('un--dropAllNS'(V2)) end(E0, E1)); _ -> V0 end.
'un--asName'(V0, V1, V2) -> case V2 of {'Idris.Core.Name.DN', E0, E1} -> (fun (V3, V4) -> {'Idris.Core.Name.DN', V3, ('un--asName'(V0, V1, V4))} end(E0, E1)); {'Idris.Core.Name.NS', E2, E3} -> (fun (V5, V6) -> {'Idris.Core.Name.NS', ('Idris.Idris2.Core.Name.Namespace':'un--replace'(V0, V1, V5)), V6} end(E2, E3)); _ -> V2 end.