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.Prelude.Types.List.erl
Raw

src/Idris.Idris2.Prelude.Types.List.erl 

-module('Idris.Idris2.Prelude.Types.List').

-compile('no_auto_import').

-compile('inline').

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

-export([

  'un--length'/2,

  'un--++'/3

]).

'un--length'(V0, V1) -> case V1 of [] -> 0; [E0 | E1] -> (fun (V2, V3) -> (1 + ('un--length'('erased', V3))) end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--++'(V0, V1, V2) -> case V1 of [] -> V2; [E0 | E1] -> (fun (V3, V4) -> [V3 | ('un--++'('erased', V4, V2))] end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.