idris2

-module('Idris.Idris2.Core.Core.Binder').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'un--traverse'/4
]).
'un--traverse'(V0, V1, V2, V3) -> case V3 of {'Idris.Core.TT.Lam', E0, E1, E2, E3} -> (fun (V4, V5, V6, V7) -> fun (V8) -> begin (V9 = (('Idris.Idris2.Core.Core.PiInfo':'un--traverse'('erased', 'erased', V2, V6))(V8))), case V9 of {'Idris.Prelude.Types.Left', E4} -> (fun (V10) -> {'Idris.Prelude.Types.Left', V10} end(E4)); {'Idris.Prelude.Types.Right', E5} -> (fun (V11) -> begin (V12 = ((V2(V7))(V8))), case V12 of {'Idris.Prelude.Types.Left', E6} -> (fun (V13) -> {'Idris.Prelude.Types.Left', V13} end(E6)); {'Idris.Prelude.Types.Right', E7} -> (fun (V14) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Lam', V4, V5, V11, V14}} end(E7)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E5)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E0, E1, E2, E3)); {'Idris.Core.TT.Let', E8, E9, E10, E11} -> (fun (V15, V16, V17, V18) -> fun (V19) -> begin (V20 = ((V2(V17))(V19))), case V20 of {'Idris.Prelude.Types.Left', E12} -> (fun (V21) -> {'Idris.Prelude.Types.Left', V21} end(E12)); {'Idris.Prelude.Types.Right', E13} -> (fun (V22) -> begin (V23 = ((V2(V18))(V19))), case V23 of {'Idris.Prelude.Types.Left', E14} -> (fun (V24) -> {'Idris.Prelude.Types.Left', V24} end(E14)); {'Idris.Prelude.Types.Right', E15} -> (fun (V25) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Let', V15, V16, V22, V25}} end(E15)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E13)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E8, E9, E10, E11)); {'Idris.Core.TT.Pi', E16, E17, E18, E19} -> (fun (V26, V27, V28, V29) -> fun (V30) -> begin (V31 = (('Idris.Idris2.Core.Core.PiInfo':'un--traverse'('erased', 'erased', V2, V28))(V30))), case V31 of {'Idris.Prelude.Types.Left', E20} -> (fun (V32) -> {'Idris.Prelude.Types.Left', V32} end(E20)); {'Idris.Prelude.Types.Right', E21} -> (fun (V33) -> begin (V34 = ((V2(V29))(V30))), case V34 of {'Idris.Prelude.Types.Left', E22} -> (fun (V35) -> {'Idris.Prelude.Types.Left', V35} end(E22)); {'Idris.Prelude.Types.Right', E23} -> (fun (V36) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.Pi', V26, V27, V33, V36}} end(E23)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E21)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E16, E17, E18, E19)); {'Idris.Core.TT.PVar', E24, E25, E26, E27} -> (fun (V37, V38, V39, V40) -> fun (V41) -> begin (V42 = (('Idris.Idris2.Core.Core.PiInfo':'un--traverse'('erased', 'erased', V2, V39))(V41))), case V42 of {'Idris.Prelude.Types.Left', E28} -> (fun (V43) -> {'Idris.Prelude.Types.Left', V43} end(E28)); {'Idris.Prelude.Types.Right', E29} -> (fun (V44) -> begin (V45 = ((V2(V40))(V41))), case V45 of {'Idris.Prelude.Types.Left', E30} -> (fun (V46) -> {'Idris.Prelude.Types.Left', V46} end(E30)); {'Idris.Prelude.Types.Right', E31} -> (fun (V47) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PVar', V37, V38, V44, V47}} end(E31)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E29)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E24, E25, E26, E27)); {'Idris.Core.TT.PLet', E32, E33, E34, E35} -> (fun (V48, V49, V50, V51) -> fun (V52) -> begin (V53 = ((V2(V50))(V52))), case V53 of {'Idris.Prelude.Types.Left', E36} -> (fun (V54) -> {'Idris.Prelude.Types.Left', V54} end(E36)); {'Idris.Prelude.Types.Right', E37} -> (fun (V55) -> begin (V56 = ((V2(V51))(V52))), case V56 of {'Idris.Prelude.Types.Left', E38} -> (fun (V57) -> {'Idris.Prelude.Types.Left', V57} end(E38)); {'Idris.Prelude.Types.Right', E39} -> (fun (V58) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PLet', V48, V49, V55, V58}} end(E39)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end(E37)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E32, E33, E34, E35)); {'Idris.Core.TT.PVTy', E40, E41, E42} -> (fun (V59, V60, V61) -> fun (V62) -> begin (V63 = ((V2(V61))(V62))), case V63 of {'Idris.Prelude.Types.Left', E43} -> (fun (V64) -> {'Idris.Prelude.Types.Left', V64} end(E43)); {'Idris.Prelude.Types.Right', E44} -> (fun (V65) -> {'Idris.Prelude.Types.Right', {'Idris.Core.TT.PVTy', V59, V60, V65}} end(E44)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end(E40, E41, E42)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.