idris2

-module('Idris.Idris2.TTImp.BindImplicits').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--bindTypeNamesUsed-4936'/5,
  'case--bindTypeNames-4894'/5,
  'case--getUsing-4750'/6,
  'case--getUsing-4684'/6,
  'case--bindNames-4608'/4,
  'case--doBind-4539'/7,
  'case--doBind-4494'/7,
  'case--renameIBinds-4392'/5,
  'case--renameIBinds-3938'/9,
  'nested--6693-4825--in--un--tag'/5,
  'nested--5745-4322--in--un--renameAlt'/6,
  'nested--6846-4967--in--un--piBind'/5,
  'nested--6293-4590--in--un--doBindAlt'/5,
  'un--renameIBinds'/3,
  'un--piBindNames'/3,
  'un--getUsings'/2,
  'un--getUsing'/2,
  'un--doBind'/2,
  'un--bindUsings'/2,
  'un--bindTypeNamesUsed'/5,
  'un--bindTypeNames'/5,
  'un--bindNames'/4,
  'un--addUsing'/2
]).
'case--bindTypeNamesUsed-4936'(V0, V1, V2, V3, V4) -> case V4 of 0 -> begin (V25 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V5) -> fun (V6) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V7) -> fun (V8) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V7, V8)) end end, fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V9, V10)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V11, V12)) end end, fun (V13) -> fun (V14) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V13, V14)) end end}, V5, V6)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V17, V18)) end end, fun (V19) -> fun (V20) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V19, V20)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V21) -> fun (V22) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V21, V22)) end end, fun (V23) -> fun (V24) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V23, V24)) end end}, V15, V16)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(0, V1, V2, V0))))), fun (V26) -> {'Idris.Prelude.Types.Right', ('un--doBind'(V25, V0))} end end; 1 -> fun (V27) -> {'Idris.Prelude.Types.Right', V0} end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--bindTypeNames-4894'(V0, V1, V2, V3, V4) -> case V4 of 0 -> begin (V25 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V5) -> fun (V6) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V7) -> fun (V8) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V7, V8)) end end, fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V9, V10)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V11, V12)) end end, fun (V13) -> fun (V14) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V13, V14)) end end}, V5, V6)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V17, V18)) end end, fun (V19) -> fun (V20) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V19, V20)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V21) -> fun (V22) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V21, V22)) end end, fun (V23) -> fun (V24) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V23, V24)) end end}, V15, V16)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(0, V1, [], V0))))), begin (V26 = ('un--doBind'(V25, V0))), fun (V27) -> {'Idris.Prelude.Types.Right', ('un--addUsing'(V2, V26))} end end end; 1 -> fun (V28) -> {'Idris.Prelude.Types.Right', V0} end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--getUsing-4750'(V0, V1, V2, V3, V4, V5) -> case V5 of 0 -> [{'Idris.Builtin.MkPair', V0, {'Idris.Builtin.MkPair', ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--top_Top__ZeroOneOmega'()), {'Idris.Builtin.MkPair', {'Idris.Core.TT.AutoImplicit'}, {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Nothing'}, V1}}}} | ('un--getUsing'(V3, V2))]; 1 -> ('un--getUsing'(V3, V2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--getUsing-4684'(V0, V1, V2, V3, V4, V5) -> case V5 of 0 -> [{'Idris.Builtin.MkPair', V0, {'Idris.Builtin.MkPair', ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'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.Builtin.MkPair', {'Idris.Core.TT.Implicit'}, {'Idris.Builtin.MkPair', {'Idris.Prelude.Types.Just', V4}, V2}}}} | ('un--getUsing'(V4, V3))]; 1 -> ('un--getUsing'(V4, V3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--bindNames-4608'(V0, V1, V2, V3) -> case V3 of 0 -> begin (V24 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V4) -> fun (V5) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V6, V7)) end end, fun (V8) -> fun (V9) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V8, V9)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V12, V13)) end end}, V4, V5)) end end, fun (V14) -> fun (V15) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V16) -> fun (V17) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V16, V17)) end end, fun (V18) -> fun (V19) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V18, V19)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V20, V21)) end end, fun (V22) -> fun (V23) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V22, V23)) end end}, V14, V15)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(V1, [], [], V0))))), fun (V25) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V26) -> {'Idris.Core.Name.UN', V26} end, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V27) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V27)) end, V24)))), ('un--doBind'(V24, V0))}} end end; 1 -> fun (V28) -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', [], V0}} end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--doBind-4539'(V0, V1, V2, V3, V4, V5, V6) -> case V2 of {'Idris.Prelude.Types.Just', E0} -> (fun (V7) -> case V7 of {'Idris.Core.Name.UN', E1} -> (fun (V8) -> ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V9) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V9)), V8)) end, V6)) end(E1)); _ -> V6 end end(E0)); _ -> V6 end.
'case--doBind-4494'(V0, V1, V2, V3, V4, V5, V6) -> case V2 of {'Idris.Prelude.Types.Just', E0} -> (fun (V7) -> case V7 of {'Idris.Core.Name.UN', E1} -> (fun (V8) -> ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V9) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V9)), V8)) end, V6)) end(E1)); _ -> V6 end end(E0)); _ -> V6 end.
'case--renameIBinds-4392'(V0, V1, V2, V3, V4) -> case V4 of 0 -> begin (V5 = ('Idris.Idris2.TTImp.Utils':'un--getUnique'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V3, V2)), V0))), fun (V6) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V7) -> fun (V8) -> fun (V9) -> fun (V10) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V9, V10)) end end end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V12)) end end, fun (V13) -> fun (V14) -> fun (V15) -> fun (V16) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V15, V16)) end end end end}, fun (V17) -> fun (V18) -> fun (V19) -> fun (V20) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V19, V20)) end end end end, fun (V21) -> fun (V22) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V22)) end end}, fun (V23) -> ('Idris.Idris2.Control.Monad.State':'dn--un--get_MonadState__$stateType_((StateT $stateType) $m)'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V26, V27)) end end end end, fun (V28) -> fun (V29) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V29)) end end, fun (V30) -> fun (V31) -> fun (V32) -> fun (V33) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V32, V33)) end end end end}, fun (V34) -> fun (V35) -> fun (V36) -> fun (V37) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V36, V37)) end end end end, fun (V38) -> fun (V39) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V39)) end end}, V23)) end, fun (V40) -> fun (V41) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V42) -> fun (V43) -> fun (V44) -> fun (V45) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V44, V45)) end end end end, fun (V46) -> fun (V47) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V47)) end end, fun (V48) -> fun (V49) -> fun (V50) -> fun (V51) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V50, V51)) end end end end}, fun (V52) -> fun (V53) -> fun (V54) -> fun (V55) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V54, V55)) end end end end, fun (V56) -> fun (V57) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V57)) end end}, fun (V58) -> ('Idris.Idris2.Control.Monad.State':'dn--un--put_MonadState__$stateType_((StateT $stateType) $m)'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V59) -> fun (V60) -> fun (V61) -> fun (V62) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V61, V62)) end end end end, fun (V63) -> fun (V64) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V64)) end end, fun (V65) -> fun (V66) -> fun (V67) -> fun (V68) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V67, V68)) end end end end}, fun (V69) -> fun (V70) -> fun (V71) -> fun (V72) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V71, V72)) end end end end, fun (V73) -> fun (V74) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V74)) end end}, [{'Idris.Builtin.MkPair', V0, V5} | V40], V58)) end, fun (V75) -> fun (V76) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V77) -> fun (V78) -> fun (V79) -> fun (V80) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V79, V80)) end end end end, fun (V81) -> fun (V82) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V82)) end end, fun (V83) -> fun (V84) -> fun (V85) -> fun (V86) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V85, V86)) end end end end}, fun (V87) -> fun (V88) -> fun (V89) -> fun (V90) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V89, V90)) end end end end, fun (V91) -> fun (V92) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V92)) end end}, {'Idris.TTImp.TTImp.IBindVar', V1, V5}, V76)) end end, V41)) end end, V6)) end end; 1 -> fun (V93) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V94) -> fun (V95) -> fun (V96) -> fun (V97) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V96, V97)) end end end end, fun (V98) -> fun (V99) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V99)) end end, fun (V100) -> fun (V101) -> fun (V102) -> fun (V103) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V102, V103)) end end end end}, fun (V104) -> fun (V105) -> fun (V106) -> fun (V107) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V106, V107)) end end end end, fun (V108) -> fun (V109) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V109)) end end}, {'Idris.TTImp.TTImp.IBindVar', V1, V0}, V93)) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--renameIBinds-3938'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V8 of 0 -> begin (V9 = ('Idris.Idris2.TTImp.Utils':'un--getUnique'(('Idris.Idris2.Prelude.Types.List':'un--++'('erased', V7, V6)), V0))), begin (V12 = ('Idris.Idris2.TTImp.Utils':'un--substNames'(('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V10) -> {'Idris.Core.Name.UN', V10} end, ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V11) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V11, V0)) end, V6)))), [{'Idris.Builtin.MkPair', {'Idris.Core.Name.UN', V0}, {'Idris.TTImp.TTImp.IVar', V5, {'Idris.Core.Name.UN', V9}}} | []], V1))), fun (V13) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V14) -> fun (V15) -> fun (V16) -> fun (V17) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V16, V17)) end end end end, fun (V18) -> fun (V19) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V19)) end end, fun (V20) -> fun (V21) -> fun (V22) -> fun (V23) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V22, V23)) end end end end}, fun (V24) -> fun (V25) -> fun (V26) -> fun (V27) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V26, V27)) end end end end, fun (V28) -> fun (V29) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V29)) end end}, ('un--renameIBinds'(V7, [V9 | V6], V12)), fun (V30) -> fun (V31) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V34, V35)) end end end end, fun (V36) -> fun (V37) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V37)) end end, fun (V38) -> fun (V39) -> fun (V40) -> fun (V41) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V40, V41)) end end end end}, fun (V42) -> fun (V43) -> fun (V44) -> fun (V45) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V44, V45)) end end end end, fun (V46) -> fun (V47) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V47)) end end}, ('un--renameIBinds'(V7, V6, V2)), fun (V48) -> fun (V49) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V50) -> fun (V51) -> fun (V52) -> fun (V53) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V52, V53)) end end end end, fun (V54) -> fun (V55) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V55)) end end, fun (V56) -> fun (V57) -> fun (V58) -> fun (V59) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V58, V59)) end end end end}, fun (V60) -> fun (V61) -> fun (V62) -> fun (V63) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V62, V63)) end end end end, fun (V64) -> fun (V65) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V65)) end end}, fun (V66) -> ('Idris.Idris2.Control.Monad.State':'dn--un--get_MonadState__$stateType_((StateT $stateType) $m)'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V67) -> fun (V68) -> fun (V69) -> fun (V70) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V69, V70)) end end end end, fun (V71) -> fun (V72) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V72)) end end, fun (V73) -> fun (V74) -> fun (V75) -> fun (V76) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V75, V76)) end end end end}, fun (V77) -> fun (V78) -> fun (V79) -> fun (V80) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V79, V80)) end end end end, fun (V81) -> fun (V82) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V82)) end end}, V66)) end, fun (V83) -> fun (V84) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V85) -> fun (V86) -> fun (V87) -> fun (V88) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V87, V88)) end end end end, fun (V89) -> fun (V90) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V90)) end end, fun (V91) -> fun (V92) -> fun (V93) -> fun (V94) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V93, V94)) end end end end}, fun (V95) -> fun (V96) -> fun (V97) -> fun (V98) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V97, V98)) end end end end, fun (V99) -> fun (V100) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V100)) end end}, fun (V101) -> ('Idris.Idris2.Control.Monad.State':'dn--un--put_MonadState__$stateType_((StateT $stateType) $m)'('erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V102) -> fun (V103) -> fun (V104) -> fun (V105) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V104, V105)) end end end end, fun (V106) -> fun (V107) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V107)) end end, fun (V108) -> fun (V109) -> fun (V110) -> fun (V111) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V110, V111)) end end end end}, fun (V112) -> fun (V113) -> fun (V114) -> fun (V115) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V114, V115)) end end end end, fun (V116) -> fun (V117) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V117)) end end}, [{'Idris.Builtin.MkPair', V0, V9} | V83], V101)) end, fun (V118) -> fun (V119) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V120) -> fun (V121) -> fun (V122) -> fun (V123) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V122, V123)) end end end end, fun (V124) -> fun (V125) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V125)) end end, fun (V126) -> fun (V127) -> fun (V128) -> fun (V129) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V128, V129)) end end end end}, fun (V130) -> fun (V131) -> fun (V132) -> fun (V133) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V132, V133)) end end end end, fun (V134) -> fun (V135) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V135)) end end}, {'Idris.TTImp.TTImp.IPi', V5, V4, V3, {'Idris.Prelude.Types.Just', {'Idris.Core.Name.UN', V9}}, V48, V30}, V119)) end end, V84)) end end, V49)) end end, V31)) end end, V13)) end end end; 1 -> fun (V136) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V137) -> fun (V138) -> fun (V139) -> fun (V140) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V139, V140)) end end end end, fun (V141) -> fun (V142) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V142)) end end, fun (V143) -> fun (V144) -> fun (V145) -> fun (V146) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V145, V146)) end end end end}, fun (V147) -> fun (V148) -> fun (V149) -> fun (V150) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V149, V150)) end end end end, fun (V151) -> fun (V152) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V152)) end end}, ('un--renameIBinds'(V7, V6, V1)), fun (V153) -> fun (V154) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V155) -> fun (V156) -> fun (V157) -> fun (V158) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V157, V158)) end end end end, fun (V159) -> fun (V160) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V160)) end end, fun (V161) -> fun (V162) -> fun (V163) -> fun (V164) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V163, V164)) end end end end}, fun (V165) -> fun (V166) -> fun (V167) -> fun (V168) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V167, V168)) end end end end, fun (V169) -> fun (V170) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V170)) end end}, ('un--renameIBinds'(V7, V6, V2)), fun (V171) -> fun (V172) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V173) -> fun (V174) -> fun (V175) -> fun (V176) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V175, V176)) end end end end, fun (V177) -> fun (V178) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V178)) end end, fun (V179) -> fun (V180) -> fun (V181) -> fun (V182) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V181, V182)) end end end end}, fun (V183) -> fun (V184) -> fun (V185) -> fun (V186) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V185, V186)) end end end end, fun (V187) -> fun (V188) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V188)) end end}, {'Idris.TTImp.TTImp.IPi', V5, V4, V3, {'Idris.Prelude.Types.Just', {'Idris.Core.Name.UN', V0}}, V171, V153}, V172)) end end, V154)) end end, V136)) end; _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--6693-4825--in--un--tag'(V0, V1, V2, V3, V4) -> case V4 of [] -> []; [E0 | E1] -> (fun (V5, V6) -> [{'Idris.Builtin.MkPair', V3, V5} | ('nested--6693-4825--in--un--tag'(V0, V1, 'erased', ((V3 + 1) rem 9223372036854775808), V6))] end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--5745-4322--in--un--renameAlt'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.TTImp.TTImp.UniqueDefault', E0} -> (fun (V6) -> fun (V7) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V8) -> fun (V9) -> fun (V10) -> fun (V11) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V10, V11)) end end end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V13)) end end, fun (V14) -> fun (V15) -> fun (V16) -> fun (V17) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V16, V17)) end end end end}, fun (V18) -> fun (V19) -> fun (V20) -> fun (V21) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V20, V21)) end end end end, fun (V22) -> fun (V23) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V23)) end end}, ('un--renameIBinds'(V4, V3, V6)), fun (V24) -> fun (V25) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V26) -> fun (V27) -> fun (V28) -> fun (V29) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V28, V29)) end end end end, fun (V30) -> fun (V31) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V31)) end end, fun (V32) -> fun (V33) -> fun (V34) -> fun (V35) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V34, V35)) end end end end}, fun (V36) -> fun (V37) -> fun (V38) -> fun (V39) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V38, V39)) end end end end, fun (V40) -> fun (V41) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V41)) end end}, {'Idris.TTImp.TTImp.UniqueDefault', V24}, V25)) end end, V7)) end end(E0)); _ -> fun (V42) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V43) -> fun (V44) -> fun (V45) -> fun (V46) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V45, V46)) end end end end, fun (V47) -> fun (V48) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V48)) end end, fun (V49) -> fun (V50) -> fun (V51) -> fun (V52) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V51, V52)) end end end end}, fun (V53) -> fun (V54) -> fun (V55) -> fun (V56) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V55, V56)) end end end end, fun (V57) -> fun (V58) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V58)) end end}, V5, V42)) end end.
'nested--6846-4967--in--un--piBind'(V0, V1, V2, V3, V4) -> case V3 of [] -> V4; [E0 | E1] -> (fun (V5, V6) -> {'Idris.TTImp.TTImp.IPi', V2, ('Idris.Idris2.Algebra.Semiring':'un--erased'('erased', {'Idris.Algebra.Semiring.dn--un--__mkSemiring', fun (V7) -> fun (V8) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|+|_Semiring__ZeroOneOmega'(V7, V8)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--plusNeutral_Semiring__ZeroOneOmega'()), fun (V9) -> fun (V10) -> ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--|*|_Semiring__ZeroOneOmega'(V9, V10)) end end, ('Idris.Idris2.Algebra.ZeroOneOmega':'dn--un--timesNeutral_Semiring__ZeroOneOmega'())})), {'Idris.Core.TT.Implicit'}, {'Idris.Prelude.Types.Just', {'Idris.Core.Name.UN', V5}}, {'Idris.TTImp.TTImp.Implicit', V2, 1}, ('nested--6846-4967--in--un--piBind'(V0, V1, V2, V6, V4))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'nested--6293-4590--in--un--doBindAlt'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.TTImp.TTImp.UniqueDefault', E0} -> (fun (V5) -> {'Idris.TTImp.TTImp.UniqueDefault', ('un--doBind'(V3, V5))} end(E0)); _ -> V4 end.
'un--renameIBinds'(V0, V1, V2) -> case V2 of {'Idris.TTImp.TTImp.IPi', E0, E1, E2, E3, E4, E5} -> (fun (V3, V4, V5, V6, V7, V8) -> case V6 of {'Idris.Prelude.Types.Just', E6} -> (fun (V9) -> case V9 of {'Idris.Core.Name.UN', E7} -> (fun (V10) -> ('case--renameIBinds-3938'(V10, V8, V7, V5, V4, V3, V1, V0, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V11, V12)) end end, fun (V13) -> fun (V14) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V13, V14)) end end}, V10, V0)))) end(E7)); _ -> fun (V15) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V16) -> fun (V17) -> fun (V18) -> fun (V19) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V18, V19)) end end end end, fun (V20) -> fun (V21) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V21)) end end, fun (V22) -> fun (V23) -> fun (V24) -> fun (V25) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V24, V25)) end end end end}, fun (V26) -> fun (V27) -> fun (V28) -> fun (V29) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V28, V29)) end end end end, fun (V30) -> fun (V31) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V31)) end end}, ('un--renameIBinds'(V0, V1, V7)), fun (V32) -> fun (V33) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V34) -> fun (V35) -> fun (V36) -> fun (V37) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V36, V37)) end end end end, fun (V38) -> fun (V39) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V39)) end end, fun (V40) -> fun (V41) -> fun (V42) -> fun (V43) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V42, V43)) end end end end}, fun (V44) -> fun (V45) -> fun (V46) -> fun (V47) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V46, V47)) end end end end, fun (V48) -> fun (V49) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V49)) end end}, ('un--renameIBinds'(V0, V1, V8)), fun (V50) -> fun (V51) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V52) -> fun (V53) -> fun (V54) -> fun (V55) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V54, V55)) end end end end, fun (V56) -> fun (V57) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V57)) end end, fun (V58) -> fun (V59) -> fun (V60) -> fun (V61) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V60, V61)) end end end end}, fun (V62) -> fun (V63) -> fun (V64) -> fun (V65) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V64, V65)) end end end end, fun (V66) -> fun (V67) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V67)) end end}, {'Idris.TTImp.TTImp.IPi', V3, V4, V5, V6, V32, V50}, V51)) end end, V33)) end end, V15)) end end end(E6)); _ -> fun (V68) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V69) -> fun (V70) -> fun (V71) -> fun (V72) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V71, V72)) end end end end, fun (V73) -> fun (V74) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V74)) end end, fun (V75) -> fun (V76) -> fun (V77) -> fun (V78) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V77, V78)) end end end end}, fun (V79) -> fun (V80) -> fun (V81) -> fun (V82) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V81, V82)) end end end end, fun (V83) -> fun (V84) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V84)) end end}, ('un--renameIBinds'(V0, V1, V7)), fun (V85) -> fun (V86) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V87) -> fun (V88) -> fun (V89) -> fun (V90) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V89, V90)) end end end end, fun (V91) -> fun (V92) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V92)) end end, fun (V93) -> fun (V94) -> fun (V95) -> fun (V96) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V95, V96)) end end end end}, fun (V97) -> fun (V98) -> fun (V99) -> fun (V100) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V99, V100)) end end end end, fun (V101) -> fun (V102) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V102)) end end}, ('un--renameIBinds'(V0, V1, V8)), fun (V103) -> fun (V104) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V105) -> fun (V106) -> fun (V107) -> fun (V108) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V107, V108)) end end end end, fun (V109) -> fun (V110) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V110)) end end, fun (V111) -> fun (V112) -> fun (V113) -> fun (V114) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V113, V114)) end end end end}, fun (V115) -> fun (V116) -> fun (V117) -> fun (V118) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V117, V118)) end end end end, fun (V119) -> fun (V120) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V120)) end end}, {'Idris.TTImp.TTImp.IPi', V3, V4, V5, V6, V85, V103}, V104)) end end, V86)) end end, V68)) end end end(E0, E1, E2, E3, E4, E5)); {'Idris.TTImp.TTImp.ILam', E8, E9, E10, E11, E12, E13} -> (fun (V121, V122, V123, V124, V125, V126) -> fun (V127) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V128) -> fun (V129) -> fun (V130) -> fun (V131) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V130, V131)) end end end end, fun (V132) -> fun (V133) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V133)) end end, fun (V134) -> fun (V135) -> fun (V136) -> fun (V137) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V136, V137)) end end end end}, fun (V138) -> fun (V139) -> fun (V140) -> fun (V141) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V140, V141)) end end end end, fun (V142) -> fun (V143) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V143)) end end}, ('un--renameIBinds'(V0, V1, V125)), fun (V144) -> fun (V145) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V146) -> fun (V147) -> fun (V148) -> fun (V149) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V148, V149)) end end end end, fun (V150) -> fun (V151) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V151)) end end, fun (V152) -> fun (V153) -> fun (V154) -> fun (V155) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V154, V155)) end end end end}, fun (V156) -> fun (V157) -> fun (V158) -> fun (V159) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V158, V159)) end end end end, fun (V160) -> fun (V161) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V161)) end end}, ('un--renameIBinds'(V0, V1, V126)), fun (V162) -> fun (V163) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V164) -> fun (V165) -> fun (V166) -> fun (V167) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V166, V167)) end end end end, fun (V168) -> fun (V169) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V169)) end end, fun (V170) -> fun (V171) -> fun (V172) -> fun (V173) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V172, V173)) end end end end}, fun (V174) -> fun (V175) -> fun (V176) -> fun (V177) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V176, V177)) end end end end, fun (V178) -> fun (V179) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V179)) end end}, {'Idris.TTImp.TTImp.ILam', V121, V122, V123, V124, V144, V162}, V163)) end end, V145)) end end, V127)) end end(E8, E9, E10, E11, E12, E13)); {'Idris.TTImp.TTImp.IApp', E14, E15, E16} -> (fun (V180, V181, V182) -> fun (V183) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V184) -> fun (V185) -> fun (V186) -> fun (V187) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V186, V187)) end end end end, fun (V188) -> fun (V189) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V189)) end end, fun (V190) -> fun (V191) -> fun (V192) -> fun (V193) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V192, V193)) end end end end}, fun (V194) -> fun (V195) -> fun (V196) -> fun (V197) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V196, V197)) end end end end, fun (V198) -> fun (V199) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V199)) end end}, ('un--renameIBinds'(V0, V1, V181)), fun (V200) -> fun (V201) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V202) -> fun (V203) -> fun (V204) -> fun (V205) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V204, V205)) end end end end, fun (V206) -> fun (V207) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V207)) end end, fun (V208) -> fun (V209) -> fun (V210) -> fun (V211) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V210, V211)) end end end end}, fun (V212) -> fun (V213) -> fun (V214) -> fun (V215) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V214, V215)) end end end end, fun (V216) -> fun (V217) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V217)) end end}, ('un--renameIBinds'(V0, V1, V182)), fun (V218) -> fun (V219) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V220) -> fun (V221) -> fun (V222) -> fun (V223) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V222, V223)) end end end end, fun (V224) -> fun (V225) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V225)) end end, fun (V226) -> fun (V227) -> fun (V228) -> fun (V229) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V228, V229)) end end end end}, fun (V230) -> fun (V231) -> fun (V232) -> fun (V233) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V232, V233)) end end end end, fun (V234) -> fun (V235) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V235)) end end}, {'Idris.TTImp.TTImp.IApp', V180, V200, V218}, V219)) end end, V201)) end end, V183)) end end(E14, E15, E16)); {'Idris.TTImp.TTImp.IImplicitApp', E17, E18, E19, E20} -> (fun (V236, V237, V238, V239) -> fun (V240) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V241) -> fun (V242) -> fun (V243) -> fun (V244) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V243, V244)) end end end end, fun (V245) -> fun (V246) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V246)) end end, fun (V247) -> fun (V248) -> fun (V249) -> fun (V250) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V249, V250)) end end end end}, fun (V251) -> fun (V252) -> fun (V253) -> fun (V254) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V253, V254)) end end end end, fun (V255) -> fun (V256) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V256)) end end}, ('un--renameIBinds'(V0, V1, V237)), fun (V257) -> fun (V258) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V259) -> fun (V260) -> fun (V261) -> fun (V262) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V261, V262)) end end end end, fun (V263) -> fun (V264) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V264)) end end, fun (V265) -> fun (V266) -> fun (V267) -> fun (V268) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V267, V268)) end end end end}, fun (V269) -> fun (V270) -> fun (V271) -> fun (V272) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V271, V272)) end end end end, fun (V273) -> fun (V274) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V274)) end end}, ('un--renameIBinds'(V0, V1, V239)), fun (V275) -> fun (V276) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V277) -> fun (V278) -> fun (V279) -> fun (V280) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V279, V280)) end end end end, fun (V281) -> fun (V282) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V282)) end end, fun (V283) -> fun (V284) -> fun (V285) -> fun (V286) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V285, V286)) end end end end}, fun (V287) -> fun (V288) -> fun (V289) -> fun (V290) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V289, V290)) end end end end, fun (V291) -> fun (V292) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V292)) end end}, {'Idris.TTImp.TTImp.IImplicitApp', V236, V257, V238, V275}, V276)) end end, V258)) end end, V240)) end end(E17, E18, E19, E20)); {'Idris.TTImp.TTImp.IWithApp', E21, E22, E23} -> (fun (V293, V294, V295) -> fun (V296) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V297) -> fun (V298) -> fun (V299) -> fun (V300) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V299, V300)) end end end end, fun (V301) -> fun (V302) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V302)) end end, fun (V303) -> fun (V304) -> fun (V305) -> fun (V306) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V305, V306)) end end end end}, fun (V307) -> fun (V308) -> fun (V309) -> fun (V310) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V309, V310)) end end end end, fun (V311) -> fun (V312) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V312)) end end}, ('un--renameIBinds'(V0, V1, V294)), fun (V313) -> fun (V314) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V315) -> fun (V316) -> fun (V317) -> fun (V318) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V317, V318)) end end end end, fun (V319) -> fun (V320) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V320)) end end, fun (V321) -> fun (V322) -> fun (V323) -> fun (V324) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V323, V324)) end end end end}, fun (V325) -> fun (V326) -> fun (V327) -> fun (V328) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V327, V328)) end end end end, fun (V329) -> fun (V330) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V330)) end end}, ('un--renameIBinds'(V0, V1, V295)), fun (V331) -> fun (V332) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V333) -> fun (V334) -> fun (V335) -> fun (V336) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V335, V336)) end end end end, fun (V337) -> fun (V338) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V338)) end end, fun (V339) -> fun (V340) -> fun (V341) -> fun (V342) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V341, V342)) end end end end}, fun (V343) -> fun (V344) -> fun (V345) -> fun (V346) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V345, V346)) end end end end, fun (V347) -> fun (V348) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V348)) end end}, {'Idris.TTImp.TTImp.IWithApp', V293, V313, V331}, V332)) end end, V314)) end end, V296)) end end(E21, E22, E23)); {'Idris.TTImp.TTImp.IAs', E24, E25, E26, E27} -> (fun (V349, V350, V351, V352) -> fun (V353) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V354) -> fun (V355) -> fun (V356) -> fun (V357) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V356, V357)) end end end end, fun (V358) -> fun (V359) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V359)) end end, fun (V360) -> fun (V361) -> fun (V362) -> fun (V363) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V362, V363)) end end end end}, fun (V364) -> fun (V365) -> fun (V366) -> fun (V367) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V366, V367)) end end end end, fun (V368) -> fun (V369) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V369)) end end}, ('un--renameIBinds'(V0, V1, V352)), fun (V370) -> fun (V371) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V372) -> fun (V373) -> fun (V374) -> fun (V375) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V374, V375)) end end end end, fun (V376) -> fun (V377) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V377)) end end, fun (V378) -> fun (V379) -> fun (V380) -> fun (V381) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V380, V381)) end end end end}, fun (V382) -> fun (V383) -> fun (V384) -> fun (V385) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V384, V385)) end end end end, fun (V386) -> fun (V387) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V387)) end end}, {'Idris.TTImp.TTImp.IAs', V349, V350, V351, V370}, V371)) end end, V353)) end end(E24, E25, E26, E27)); {'Idris.TTImp.TTImp.IMustUnify', E28, E29, E30} -> (fun (V388, V389, V390) -> fun (V391) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V392) -> fun (V393) -> fun (V394) -> fun (V395) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V394, V395)) end end end end, fun (V396) -> fun (V397) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V397)) end end, fun (V398) -> fun (V399) -> fun (V400) -> fun (V401) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V400, V401)) end end end end}, fun (V402) -> fun (V403) -> fun (V404) -> fun (V405) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V404, V405)) end end end end, fun (V406) -> fun (V407) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V407)) end end}, ('un--renameIBinds'(V0, V1, V390)), fun (V408) -> fun (V409) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V410) -> fun (V411) -> fun (V412) -> fun (V413) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V412, V413)) end end end end, fun (V414) -> fun (V415) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V415)) end end, fun (V416) -> fun (V417) -> fun (V418) -> fun (V419) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V418, V419)) end end end end}, fun (V420) -> fun (V421) -> fun (V422) -> fun (V423) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V422, V423)) end end end end, fun (V424) -> fun (V425) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V425)) end end}, {'Idris.TTImp.TTImp.IMustUnify', V388, V389, V408}, V409)) end end, V391)) end end(E28, E29, E30)); {'Idris.TTImp.TTImp.IDelayed', E31, E32, E33} -> (fun (V426, V427, V428) -> fun (V429) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V430) -> fun (V431) -> fun (V432) -> fun (V433) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V432, V433)) end end end end, fun (V434) -> fun (V435) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V435)) end end, fun (V436) -> fun (V437) -> fun (V438) -> fun (V439) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V438, V439)) end end end end}, fun (V440) -> fun (V441) -> fun (V442) -> fun (V443) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V442, V443)) end end end end, fun (V444) -> fun (V445) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V445)) end end}, ('un--renameIBinds'(V0, V1, V428)), fun (V446) -> fun (V447) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V448) -> fun (V449) -> fun (V450) -> fun (V451) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V450, V451)) end end end end, fun (V452) -> fun (V453) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V453)) end end, fun (V454) -> fun (V455) -> fun (V456) -> fun (V457) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V456, V457)) end end end end}, fun (V458) -> fun (V459) -> fun (V460) -> fun (V461) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V460, V461)) end end end end, fun (V462) -> fun (V463) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V463)) end end}, {'Idris.TTImp.TTImp.IDelayed', V426, V427, V446}, V447)) end end, V429)) end end(E31, E32, E33)); {'Idris.TTImp.TTImp.IDelay', E34, E35} -> (fun (V464, V465) -> fun (V466) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V467) -> fun (V468) -> fun (V469) -> fun (V470) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V469, V470)) end end end end, fun (V471) -> fun (V472) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V472)) end end, fun (V473) -> fun (V474) -> fun (V475) -> fun (V476) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V475, V476)) end end end end}, fun (V477) -> fun (V478) -> fun (V479) -> fun (V480) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V479, V480)) end end end end, fun (V481) -> fun (V482) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V482)) end end}, ('un--renameIBinds'(V0, V1, V465)), fun (V483) -> fun (V484) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V485) -> fun (V486) -> fun (V487) -> fun (V488) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V487, V488)) end end end end, fun (V489) -> fun (V490) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V490)) end end, fun (V491) -> fun (V492) -> fun (V493) -> fun (V494) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V493, V494)) end end end end}, fun (V495) -> fun (V496) -> fun (V497) -> fun (V498) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V497, V498)) end end end end, fun (V499) -> fun (V500) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V500)) end end}, {'Idris.TTImp.TTImp.IDelay', V464, V483}, V484)) end end, V466)) end end(E34, E35)); {'Idris.TTImp.TTImp.IForce', E36, E37} -> (fun (V501, V502) -> fun (V503) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V504) -> fun (V505) -> fun (V506) -> fun (V507) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V506, V507)) end end end end, fun (V508) -> fun (V509) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V509)) end end, fun (V510) -> fun (V511) -> fun (V512) -> fun (V513) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V512, V513)) end end end end}, fun (V514) -> fun (V515) -> fun (V516) -> fun (V517) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V516, V517)) end end end end, fun (V518) -> fun (V519) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V519)) end end}, ('un--renameIBinds'(V0, V1, V502)), fun (V520) -> fun (V521) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V522) -> fun (V523) -> fun (V524) -> fun (V525) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V524, V525)) end end end end, fun (V526) -> fun (V527) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V527)) end end, fun (V528) -> fun (V529) -> fun (V530) -> fun (V531) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V530, V531)) end end end end}, fun (V532) -> fun (V533) -> fun (V534) -> fun (V535) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V534, V535)) end end end end, fun (V536) -> fun (V537) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V537)) end end}, {'Idris.TTImp.TTImp.IForce', V501, V520}, V521)) end end, V503)) end end(E36, E37)); {'Idris.TTImp.TTImp.IAlternative', E38, E39, E40} -> (fun (V538, V539, V540) -> fun (V541) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V542) -> fun (V543) -> fun (V544) -> fun (V545) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V544, V545)) end end end end, fun (V546) -> fun (V547) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V547)) end end, fun (V548) -> fun (V549) -> fun (V550) -> fun (V551) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V550, V551)) end end end end}, fun (V552) -> fun (V553) -> fun (V554) -> fun (V555) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V554, V555)) end end end end, fun (V556) -> fun (V557) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V557)) end end}, ('nested--5745-4322--in--un--renameAlt'(V540, V539, V538, V1, V0, V539)), fun (V558) -> fun (V559) -> ('Idris.Idris2.Control.Monad.State':'dn--un-->>=_Monad__((StateT $stateType) $m)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V560) -> fun (V561) -> fun (V562) -> fun (V563) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V562, V563)) end end end end, fun (V564) -> fun (V565) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V565)) end end, fun (V566) -> fun (V567) -> fun (V568) -> fun (V569) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V568, V569)) end end end end}, fun (V570) -> fun (V571) -> fun (V572) -> fun (V573) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V572, V573)) end end end end, fun (V574) -> fun (V575) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V575)) end end}, ('Idris.Idris2.Prelude.Types':'dn--un--traverse_Traversable__List'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V576) -> fun (V577) -> fun (V578) -> fun (V579) -> fun (V580) -> ('Idris.Idris2.Control.Monad.State':'dn--un--map_Functor__((StateT $stateType) $f)'('erased', 'erased', 'erased', 'erased', fun (V581) -> fun (V582) -> fun (V583) -> fun (V584) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V583, V584)) end end end end, V578, V579, V580)) end end end end end, fun (V585) -> fun (V586) -> fun (V587) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V588) -> fun (V589) -> fun (V590) -> fun (V591) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V590, V591)) end end end end, fun (V592) -> fun (V593) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V593)) end end, fun (V594) -> fun (V595) -> fun (V596) -> fun (V597) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V596, V597)) end end end end}, fun (V598) -> fun (V599) -> fun (V600) -> fun (V601) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V600, V601)) end end end end, fun (V602) -> fun (V603) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V603)) end end}, V586, V587)) end end end, fun (V604) -> fun (V605) -> fun (V606) -> fun (V607) -> fun (V608) -> ('Idris.Idris2.Control.Monad.State':'dn--un--<*>_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V609) -> fun (V610) -> fun (V611) -> fun (V612) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V611, V612)) end end end end, fun (V613) -> fun (V614) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V614)) end end, fun (V615) -> fun (V616) -> fun (V617) -> fun (V618) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V617, V618)) end end end end}, fun (V619) -> fun (V620) -> fun (V621) -> fun (V622) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V621, V622)) end end end end, fun (V623) -> fun (V624) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V624)) end end}, V606, V607, V608)) end end end end end}, fun (V625) -> ('un--renameIBinds'(V0, V1, V625)) end, V540)), fun (V626) -> fun (V627) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V628) -> fun (V629) -> fun (V630) -> fun (V631) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V630, V631)) end end end end, fun (V632) -> fun (V633) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V633)) end end, fun (V634) -> fun (V635) -> fun (V636) -> fun (V637) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V636, V637)) end end end end}, fun (V638) -> fun (V639) -> fun (V640) -> fun (V641) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V640, V641)) end end end end, fun (V642) -> fun (V643) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V643)) end end}, {'Idris.TTImp.TTImp.IAlternative', V538, V558, V626}, V627)) end end, V559)) end end, V541)) end end(E38, E39, E40)); {'Idris.TTImp.TTImp.IBindVar', E41, E42} -> (fun (V644, V645) -> ('case--renameIBinds-4392'(V645, V644, V1, V0, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V646) -> fun (V647) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V646, V647)) end end, fun (V648) -> fun (V649) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V648, V649)) end end}, V645, V0)))) end(E41, E42)); _ -> fun (V650) -> ('Idris.Idris2.Control.Monad.State':'dn--un--pure_Applicative__((StateT $stateType) $f)'('erased', 'erased', 'erased', {'Idris.Prelude.Interfaces.dn--un--__mkMonad', {'Idris.Prelude.Interfaces.dn--un--__mkApplicative', fun (V651) -> fun (V652) -> fun (V653) -> fun (V654) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--map_Functor__Identity'('erased', 'erased', V653, V654)) end end end end, fun (V655) -> fun (V656) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--pure_Applicative__Identity'('erased', V656)) end end, fun (V657) -> fun (V658) -> fun (V659) -> fun (V660) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--<*>_Applicative__Identity'('erased', 'erased', V659, V660)) end end end end}, fun (V661) -> fun (V662) -> fun (V663) -> fun (V664) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un-->>=_Monad__Identity'('erased', 'erased', V663, V664)) end end end end, fun (V665) -> fun (V666) -> ('Idris.Idris2.Control.Monad.Identity':'dn--un--join_Monad__Identity'('erased', V666)) end end}, V2, V650)) end end.
'un--piBindNames'(V0, V1, V2) -> begin (V23 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V3) -> fun (V4) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V5) -> fun (V6) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V5, V6)) end end, fun (V7) -> fun (V8) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V7, V8)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V11, V12)) end end}, V3, V4)) end end, fun (V13) -> fun (V14) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V15) -> fun (V16) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V15, V16)) end end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V17, V18)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V19) -> fun (V20) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V19, V20)) end end, fun (V21) -> fun (V22) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V21, V22)) end end}, V13, V14)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(0, V1, [], V2))))), ('nested--6846-4967--in--un--piBind'(V2, V1, V0, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V24) -> ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V24)) end, V23)), V2)) end.
'un--getUsings'(V0, V1) -> case V0 of [] -> []; [E0 | E1] -> (fun (V2, V3) -> ('Idris.Idris2.Prelude.Types.List':'un--++'('erased', ('un--getUsing'(V2, V1)), ('un--getUsings'(V3, V1)))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--getUsing'(V0, V1) -> case V1 of [] -> []; [E0 | E1] -> (fun (V2, V3) -> case V2 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V4, V5) -> case V5 of {'Idris.Builtin.MkPair', E4, E5} -> (fun (V6, V7) -> case V6 of {'Idris.Prelude.Types.Just', E6} -> (fun (V8) -> ('case--getUsing-4684'(V4, V8, V7, V3, V0, ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V0, V8)))) end(E6)); {'Idris.Prelude.Types.Nothing'} -> (fun () -> begin (V13 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V11, V12)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findIBindVars'(V7))))), ('case--getUsing-4750'(V4, V7, V3, V0, V13, ('Idris.Idris2.Prelude.Types':'un--elem'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V14) -> fun (V15) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V14, V15)) end end, fun (V16) -> fun (V17) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V16, V17)) end end}, V0, V13)))) end end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--doBind'(V0, V1) -> case V0 of [] -> V1; _ -> case V1 of {'Idris.TTImp.TTImp.IVar', E0, E1} -> (fun (V2, V3) -> case V3 of {'Idris.Core.Name.UN', E2} -> (fun (V4) -> ('Idris.Idris2.Prelude.Types':'un--maybe'('erased', 'erased', fun () -> {'Idris.TTImp.TTImp.IVar', V2, {'Idris.Core.Name.UN', V4}} end, fun () -> fun (V5) -> {'Idris.TTImp.TTImp.IBindVar', V2, V5} end end, ('Idris.Idris2.Data.List':'un--lookup'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V6) -> fun (V7) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V6, V7)) end end, fun (V8) -> fun (V9) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V8, V9)) end end}, V4, V0)))) end(E2)); _ -> V1 end end(E0, E1)); {'Idris.TTImp.TTImp.IPi', E3, E4, E5, E6, E7, E8} -> (fun (V10, V11, V12, V13, V14, V15) -> begin (V19 = case V13 of {'Idris.Prelude.Types.Just', E9} -> (fun (V16) -> case V16 of {'Idris.Core.Name.UN', E10} -> (fun (V17) -> ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V18) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V18)), V17)) end, V0)) end(E10)); _ -> V0 end end(E9)); _ -> V0 end), {'Idris.TTImp.TTImp.IPi', V10, V11, V12, V13, ('un--doBind'(V19, V14)), ('un--doBind'(V19, V15))} end end(E3, E4, E5, E6, E7, E8)); {'Idris.TTImp.TTImp.ILam', E11, E12, E13, E14, E15, E16} -> (fun (V20, V21, V22, V23, V24, V25) -> begin (V29 = case V23 of {'Idris.Prelude.Types.Just', E17} -> (fun (V26) -> case V26 of {'Idris.Core.Name.UN', E18} -> (fun (V27) -> ('Idris.Idris2.Data.List':'un--filter'('erased', fun (V28) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V28)), V27)) end, V0)) end(E18)); _ -> V0 end end(E17)); _ -> V0 end), {'Idris.TTImp.TTImp.ILam', V20, V21, V22, V23, ('un--doBind'(V29, V24)), ('un--doBind'(V29, V25))} end end(E11, E12, E13, E14, E15, E16)); {'Idris.TTImp.TTImp.IApp', E19, E20, E21} -> (fun (V30, V31, V32) -> {'Idris.TTImp.TTImp.IApp', V30, ('un--doBind'(V0, V31)), ('un--doBind'(V0, V32))} end(E19, E20, E21)); {'Idris.TTImp.TTImp.IImplicitApp', E22, E23, E24, E25} -> (fun (V33, V34, V35, V36) -> {'Idris.TTImp.TTImp.IImplicitApp', V33, ('un--doBind'(V0, V34)), V35, ('un--doBind'(V0, V36))} end(E22, E23, E24, E25)); {'Idris.TTImp.TTImp.IWithApp', E26, E27, E28} -> (fun (V37, V38, V39) -> {'Idris.TTImp.TTImp.IWithApp', V37, ('un--doBind'(V0, V38)), ('un--doBind'(V0, V39))} end(E26, E27, E28)); {'Idris.TTImp.TTImp.IAs', E29, E30, E31, E32} -> (fun (V40, V41, V42, V43) -> {'Idris.TTImp.TTImp.IAs', V40, V41, V42, ('un--doBind'(V0, V43))} end(E29, E30, E31, E32)); {'Idris.TTImp.TTImp.IMustUnify', E33, E34, E35} -> (fun (V44, V45, V46) -> {'Idris.TTImp.TTImp.IMustUnify', V44, V45, ('un--doBind'(V0, V46))} end(E33, E34, E35)); {'Idris.TTImp.TTImp.IDelayed', E36, E37, E38} -> (fun (V47, V48, V49) -> {'Idris.TTImp.TTImp.IDelayed', V47, V48, ('un--doBind'(V0, V49))} end(E36, E37, E38)); {'Idris.TTImp.TTImp.IDelay', E39, E40} -> (fun (V50, V51) -> {'Idris.TTImp.TTImp.IDelay', V50, ('un--doBind'(V0, V51))} end(E39, E40)); {'Idris.TTImp.TTImp.IForce', E41, E42} -> (fun (V52, V53) -> {'Idris.TTImp.TTImp.IForce', V52, ('un--doBind'(V0, V53))} end(E41, E42)); {'Idris.TTImp.TTImp.IQuote', E43, E44} -> (fun (V54, V55) -> {'Idris.TTImp.TTImp.IQuote', V54, ('un--doBind'(V0, V55))} end(E43, E44)); {'Idris.TTImp.TTImp.IUnquote', E45, E46} -> (fun (V56, V57) -> {'Idris.TTImp.TTImp.IUnquote', V56, ('un--doBind'(V0, V57))} end(E45, E46)); {'Idris.TTImp.TTImp.IAlternative', E47, E48, E49} -> (fun (V58, V59, V60) -> {'Idris.TTImp.TTImp.IAlternative', V58, ('nested--6293-4590--in--un--doBindAlt'(V60, V59, V58, V0, V59)), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V61) -> ('un--doBind'(V0, V61)) end, V60))} end(E47, E48, E49)); _ -> V1 end end.
'un--bindUsings'(V0, V1) -> case V0 of [] -> V1; [E0 | E1] -> (fun (V2, V3) -> case V2 of {'Idris.Builtin.MkPair', E2, E3} -> (fun (V4, V5) -> case V5 of {'Idris.Builtin.MkPair', E4, E5} -> (fun (V6, V7) -> case V7 of {'Idris.Builtin.MkPair', E6, E7} -> (fun (V8, V9) -> {'Idris.TTImp.TTImp.IPi', ('Idris.Idris2.TTImp.TTImp':'un--getFC'(V9)), V4, V6, V8, V9, ('un--bindUsings'(V3, V1))} end(E6, E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E4, E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--bindTypeNamesUsed'(V0, V1, V2, V3, V4) -> begin (V5 = ('Idris.Idris2.Core.Context':'un--isUnboundImplicits'(V0, V4))), case V5 of {'Idris.Prelude.Types.Left', E0} -> (fun (V6) -> {'Idris.Prelude.Types.Left', V6} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V7) -> case V7 of 0 -> begin (V28 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V8) -> fun (V9) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V12, V13)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V14) -> fun (V15) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V14, V15)) end end, fun (V16) -> fun (V17) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V16, V17)) end end}, V8, V9)) end end, fun (V18) -> fun (V19) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V20, V21)) end end, fun (V22) -> fun (V23) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V22, V23)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V24) -> fun (V25) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V24, V25)) end end, fun (V26) -> fun (V27) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V26, V27)) end end}, V18, V19)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(0, V2, V1, V3))))), {'Idris.Prelude.Types.Right', ('un--doBind'(V28, V3))} end; 1 -> {'Idris.Prelude.Types.Right', V3}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--bindTypeNames'(V0, V1, V2, V3, V4) -> begin (V5 = ('Idris.Idris2.Core.Context':'un--isUnboundImplicits'(V0, V4))), case V5 of {'Idris.Prelude.Types.Left', E0} -> (fun (V6) -> {'Idris.Prelude.Types.Left', V6} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V7) -> case V7 of 0 -> begin (V28 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V8) -> fun (V9) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V10) -> fun (V11) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V10, V11)) end end, fun (V12) -> fun (V13) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V12, V13)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V14) -> fun (V15) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V14, V15)) end end, fun (V16) -> fun (V17) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V16, V17)) end end}, V8, V9)) end end, fun (V18) -> fun (V19) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V20) -> fun (V21) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V20, V21)) end end, fun (V22) -> fun (V23) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V22, V23)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V24) -> fun (V25) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V24, V25)) end end, fun (V26) -> fun (V27) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V26, V27)) end end}, V18, V19)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(0, V2, [], V3))))), begin (V29 = ('un--doBind'(V28, V3))), {'Idris.Prelude.Types.Right', ('un--addUsing'(V1, V29))} end end; 1 -> {'Idris.Prelude.Types.Right', V3}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--bindNames'(V0, V1, V2, V3) -> begin (V4 = ('Idris.Idris2.Core.Context':'un--isUnboundImplicits'(V0, V3))), case V4 of {'Idris.Prelude.Types.Left', E0} -> (fun (V5) -> {'Idris.Prelude.Types.Left', V5} end(E0)); {'Idris.Prelude.Types.Right', E1} -> (fun (V6) -> case V6 of 0 -> begin (V27 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V7) -> fun (V8) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V9) -> fun (V10) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V9, V10)) end end, fun (V11) -> fun (V12) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V11, V12)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V13) -> fun (V14) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V13, V14)) end end, fun (V15) -> fun (V16) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V15, V16)) end end}, V7, V8)) end end, fun (V17) -> fun (V18) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__(|((Builtin.Pair $a) $b),((Builtin.MkPair $a) $b)|)'('erased', 'erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V19) -> fun (V20) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V19, V20)) end end, fun (V21) -> fun (V22) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V21, V22)) end end}, {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V23) -> fun (V24) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__String'(V23, V24)) end end, fun (V25) -> fun (V26) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--/=_Eq__String'(V25, V26)) end end}, V17, V18)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findBindableNames'(V1, [], [], V2))))), {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V28) -> {'Idris.Core.Name.UN', V28} end, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V29) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V29)) end, V27)))), ('un--doBind'(V27, V2))}} end; 1 -> {'Idris.Prelude.Types.Right', {'Idris.Builtin.MkPair', [], V2}}; _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--addUsing'(V0, V1) -> begin (V6 = ('Idris.Idris2.Data.List':'un--nub'('erased', {'Idris.Prelude.EqOrd.dn--un--__mkEq', fun (V2) -> fun (V3) -> ('Idris.Idris2.Core.Name':'dn--un--==_Eq__Name'(V2, V3)) end end, fun (V4) -> fun (V5) -> ('Idris.Idris2.Core.Name':'dn--un--/=_Eq__Name'(V4, V5)) end end}, ('Idris.Idris2.TTImp.Utils':'un--findIBindVars'(V1))))), begin (V9 = ('Idris.Idris2.Data.List':'un--nubBy'('erased', fun (V7) -> fun (V8) -> ('Idris.Idris2.Prelude.EqOrd':'dn--un--==_Eq__Int'(('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V7)), ('Idris.Idris2.Builtin':'un--fst'('erased', 'erased', V8)))) end end, ('un--getUsings'(V6, ('nested--6693-4825--in--un--tag'(V1, V0, 'erased', 0, V0))))))), ('un--bindUsings'(('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V10) -> ('Idris.Idris2.Builtin':'un--snd'('erased', 'erased', V10)) end, V9)), V1)) end end.