idris2

-module('Idris.Idris2.Data.Primitives.Views.IntV').
-compile('no_auto_import').
-compile('inline').
-compile({'inline_size',24}).
-export([
  'case--intRec-454'/2,
  'case--divides-392'/3,
  'un--intRec'/1,
  'un--divides'/2
]).
'case--intRec-454'(V0, V1) -> case V1 of 0 -> {'Idris.Data.Primitives.Views.IntV.IntSucc', ('un--intRec'(('Idris.Idris2.Prelude.Num':'dn--un---_Neg__Int'(V0, 1))))}; 1 -> ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', {'Idris.Data.Primitives.Views.IntV.IntPred', ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', ('un--intRec'(((V0 + 1) rem 9223372036854775808)))))})); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'case--divides-392'(V0, V1, V2) -> case V2 of 0 -> ('Idris.Idris2.Prelude.Num':'dn--un--negate_Neg__Int'(('Idris.Idris2.Prelude.Num':'dn--un--div_Integral__Int'(V1, ('Idris.Idris2.Prelude.Num':'dn--un--abs_Abs__Int'(V0)))))); 1 -> ('Idris.Idris2.Prelude.Num':'dn--un--div_Integral__Int'(V1, V0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.
'un--intRec'(V0) -> case V0 of 0 -> {'Idris.Data.Primitives.Views.IntV.IntZ'}; _ -> ('case--intRec-454'(V0, ('Idris.Idris2.Prelude.EqOrd':'dn--un-->_Ord__Int'(V0, 0)))) end.
'un--divides'(V0, V1) -> case V1 of 0 -> {'Idris.Data.Primitives.Views.IntV.DivByZero'}; _ -> begin (V2 = ('case--divides-392'(V1, V0, ('Idris.Idris2.Prelude.EqOrd':'dn--un--<_Ord__Int'(V1, 0))))), begin (V3 = ('Idris.Idris2.Prelude.Num':'dn--un--abs_Abs__Int'(('Idris.Idris2.Prelude.Num':'dn--un---_Neg__Int'(V0, ((V2 * V1) rem 9223372036854775808)))))), ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', {'Idris.Data.Primitives.Views.IntV.DivBy', V2, V3, ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', {'Idris.Builtin.Refl'}))})) end end end.