idris2

-module('Idris.Idris2.Core.TT.SubstEnv').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--case block in find-8112'/11,
  'case--find-8069'/9,
  'un--substs'/4,
  'un--substEnv'/6,
  'un--subst'/4,
  'un--findDrop'/6,
  'un--find'/8
]).
'case--case block in find-8112'(V0, V1, V2, V3, V4, V5, V6, V7, V8, V9, V10) -> case V5 of 0 -> {'Idris.Core.TT.Local', V7, V6, 0}; _ -> begin (V11 = (V5 - 1)), ('Idris.Idris2.Core.TT':'dn--un--weaken_Weaken__Term'('erased', 'erased', ('un--find'('erased', 'erased', 'erased', V7, V6, V8, V11, V2)))) end end.
'case--find-8069'(V0, V1, V2, V3, V4, V5, V6, V7, V8) -> case V5 of 0 -> case V8 of {'Idris.Core.TT.SizedView.Z'} -> (fun () -> ('un--findDrop'('erased', 'erased', V7, V6, V4, V3)) end()); _ -> case V8 of {'Idris.Core.TT.SizedView.S', E1} -> (fun (V9) -> case V4 of 0 -> {'Idris.Core.TT.Local', V7, V6, 0}; _ -> begin (V10 = (V4 - 1)), ('Idris.Idris2.Core.TT':'dn--un--weaken_Weaken__Term'('erased', 'erased', ('un--find'('erased', 'erased', 'erased', V7, V6, V9, V10, V3)))) end end end(E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end; _ -> case V8 of {'Idris.Core.TT.SizedView.S', E0} -> (fun (V11) -> case V4 of 0 -> {'Idris.Core.TT.Local', V7, V6, 0}; _ -> begin (V12 = (V4 - 1)), ('Idris.Idris2.Core.TT':'dn--un--weaken_Weaken__Term'('erased', 'erased', ('un--find'('erased', 'erased', 'erased', V7, V6, V11, V12, V3)))) end end end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end.
'un--substs'(V0, V1, V2, V3) -> ('un--substEnv'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--zero'('erased')), V2, V3)).
'un--substEnv'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.Local', E0, E1, E2} -> (fun (V6, V7, V8) -> ('un--find'('erased', 'erased', 'erased', V6, V7, V3, V8, V4)) end(E0, E1, E2)); {'Idris.Core.TT.Ref', E3, E4, E5} -> (fun (V9, V10, V11) -> {'Idris.Core.TT.Ref', V9, V10, V11} end(E3, E4, E5)); {'Idris.Core.TT.Meta', E6, E7, E8, E9} -> (fun (V12, V13, V14, V15) -> {'Idris.Core.TT.Meta', V12, V13, V14, ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V16) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V16)) end, V15))} end(E6, E7, E8, E9)); {'Idris.Core.TT.Bind', E10, E11, E12, E13} -> (fun (V17, V18, V19, V20) -> {'Idris.Core.TT.Bind', V17, V18, ('Idris.Idris2.Core.TT':'dn--un--map_Functor__Binder'('erased', 'erased', fun (V21) -> ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V21)) end, V19)), ('un--substEnv'('erased', 'erased', 'erased', ('Idris.Idris2.Core.TT.SizeOf':'un--suc'('erased', 'erased', 'erased', V3)), V4, V20))} end(E10, E11, E12, E13)); {'Idris.Core.TT.App', E14, E15, E16} -> (fun (V22, V23, V24) -> {'Idris.Core.TT.App', V22, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V23)), ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V24))} end(E14, E15, E16)); {'Idris.Core.TT.As', E17, E18, E19, E20} -> (fun (V25, V26, V27, V28) -> {'Idris.Core.TT.As', V25, V26, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V27)), ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V28))} end(E17, E18, E19, E20)); {'Idris.Core.TT.TDelayed', E21, E22, E23} -> (fun (V29, V30, V31) -> {'Idris.Core.TT.TDelayed', V29, V30, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V31))} end(E21, E22, E23)); {'Idris.Core.TT.TDelay', E24, E25, E26, E27} -> (fun (V32, V33, V34, V35) -> {'Idris.Core.TT.TDelay', V32, V33, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V34)), ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V35))} end(E24, E25, E26, E27)); {'Idris.Core.TT.TForce', E28, E29, E30} -> (fun (V36, V37, V38) -> {'Idris.Core.TT.TForce', V36, V37, ('un--substEnv'('erased', 'erased', 'erased', V3, V4, V38))} end(E28, E29, E30)); {'Idris.Core.TT.PrimVal', E31, E32} -> (fun (V39, V40) -> {'Idris.Core.TT.PrimVal', V39, V40} end(E31, E32)); {'Idris.Core.TT.Erased', E33, E34} -> (fun (V41, V42) -> {'Idris.Core.TT.Erased', V41, V42} end(E33, E34)); {'Idris.Core.TT.TType', E35} -> (fun (V43) -> {'Idris.Core.TT.TType', V43} end(E35)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--subst'(V0, V1, V2, V3) -> ('un--substs'('erased', 'erased', {'Idris.Core.TT.SubstEnv.::', V2, {'Idris.Core.TT.SubstEnv.Nil'}}, V3)).
'un--findDrop'(V0, V1, V2, V3, V4, V5) -> case V5 of {'Idris.Core.TT.SubstEnv.Nil'} -> (fun () -> {'Idris.Core.TT.Local', V2, V3, V4} end()); _ -> case V4 of 0 -> case V5 of {'Idris.Core.TT.SubstEnv.::', E2, E3} -> (fun (V6, V7) -> V6 end(E2, E3)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end; _ -> begin (V8 = (V4 - 1)), case V5 of {'Idris.Core.TT.SubstEnv.::', E0, E1} -> (fun (V9, V10) -> ('un--findDrop'('erased', 'erased', V2, V3, V8, V10)) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end end.
'un--find'(V0, V1, V2, V3, V4, V5, V6, V7) -> ('case--find-8069'('erased', 'erased', 'erased', V7, V6, V5, V4, V3, ('Idris.Idris2.Core.TT':'un--sizedView'('erased', 'erased', V5)))).