Packages

idris2

0.2.1-alpha.1
0.2.1-alpha.1

Erlang code generator for Idris 2

Current section

Files

Jump to
Readme
1 Version
0 Dependencies
Dependants
Files
Activity
idris2 src Idris.Idris2.Core.TT.HasLength.erl
Raw

src/Idris.Idris2.Core.TT.HasLength.erl 

-module('Idris.Idris2.Core.TT.HasLength').

-compile('no_auto_import').

-compile('inline').

-compile({'inline_size',24}).

-export([

  'un--take'/3,

  'un--sucR'/5,

  'un--mkHasLength'/2,

  'un--hlReverseOnto'/7,

  'un--hlReverse'/4,

  'un--hlAppend'/7,

  'un--cast'/7

]).

'un--take'(V0, V1, V2) -> case V1 of 0 -> {'Idris.Core.TT.HasLength.Z'}; _ -> begin (V3 = (V1 - 1)), case V2 of {'Idris.Prelude.Types.Stream.::', E0, E1} -> (fun (V4, V5) -> {'Idris.Core.TT.HasLength.S', ('un--take'('erased', V3, (V5())))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end end.

'un--sucR'(V0, V1, V2, V3, V4) -> case V4 of {'Idris.Core.TT.HasLength.Z'} -> (fun () -> {'Idris.Core.TT.HasLength.S', {'Idris.Core.TT.HasLength.Z'}} end()); {'Idris.Core.TT.HasLength.S', E0} -> (fun (V5) -> {'Idris.Core.TT.HasLength.S', ('un--sucR'('erased', 'erased', 'erased', 'erased', V5))} end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--mkHasLength'(V0, V1) -> case V1 of [] -> {'Idris.Core.TT.HasLength.Z'}; [E0 | E1] -> (fun (V2, V3) -> {'Idris.Core.TT.HasLength.S', ('un--mkHasLength'('erased', V3))} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--hlReverseOnto'(V0, V1, V2, V3, V4, V5, V6) -> case V6 of {'Idris.Core.TT.HasLength.Z'} -> (fun () -> V5 end()); {'Idris.Core.TT.HasLength.S', E0} -> (fun (V7) -> ('un--hlReverseOnto'('erased', 'erased', 'erased', 'erased', 'erased', {'Idris.Core.TT.HasLength.S', V5}, V7)) end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--hlReverse'(V0, V1, V2, V3) -> ('un--hlReverseOnto'('erased', 'erased', 'erased', 'erased', 'erased', {'Idris.Core.TT.HasLength.Z'}, V3)).

'un--hlAppend'(V0, V1, V2, V3, V4, V5, V6) -> case V5 of {'Idris.Core.TT.HasLength.Z'} -> (fun () -> V6 end()); {'Idris.Core.TT.HasLength.S', E0} -> (fun (V7) -> {'Idris.Core.TT.HasLength.S', ('un--hlAppend'('erased', 'erased', 'erased', 'erased', 'erased', V7, V6))} end(E0)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--cast'(V0, V1, V2, V3, V4, V5, V6) -> case V4 of [] -> case V6 of {'Idris.Core.TT.HasLength.Z'} -> (fun () -> {'Idris.Core.TT.HasLength.Z'} end()); _ -> ('erlang':'throw'("Error: Unreachable branch")) end; [E0 | E1] -> (fun (V7, V8) -> case V6 of {'Idris.Core.TT.HasLength.S', E2} -> (fun (V9) -> {'Idris.Core.TT.HasLength.S', ('un--cast'('erased', 'erased', 'erased', 'erased', V8, ('Idris.Idris2.Data.Nat':'un--succInjective'('erased', 'erased', V5)), V9))} end(E2)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.