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.Erlang.Types.Map.erl
Raw

src/Idris.Idris2.Erlang.Types.Map.erl 

-module('Idris.Idris2.Erlang.Types.Map').

-compile('no_auto_import').

-compile('inline').

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

-export([

  'case--get-1371'/7,

  'case--entries-1279'/4,

  'un--values'/2,

  'un--toAnyMap'/2,

  'un--size'/2,

  'un--lookup'/7,

  'un--keys'/2,

  'un--insert'/6,

  'un--get'/6,

  'un--entries'/2,

  'un--empty'/0,

  'un--delete'/4

]).

'case--get-1371'(V0, V1, V2, V3, V4, V5, V6) -> V6.

'case--entries-1279'(V0, V1, V2, V3) -> case V3 of {E0, E1} -> (fun (V4, V5) -> {'Idris.Builtin.MkPair', V4, V5} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end.

'un--values'(V0, V1) -> ('erlang':'apply'('maps', 'values', [('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V1)) | []])).

'un--toAnyMap'(V0, V1) -> ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V1)).

'un--size'(V0, V1) -> begin (V2 = ('erlang':'apply'('maps', 'size', [('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V1)) | []]))), V2 end.

'un--lookup'(V0, V1, V2, V3, V4, V5, V6) -> ('Idris.Idris2.Erlang.Decode':'un--erlDecodeMay'('erased', 'erased', {'Idris.Erlang.Types.ETErlMapSubset', {'Idris.Erlang.Types.EMTNil'}}, fun (V7) -> ('Idris.Idris2.Erlang.Decode':'un--mapEntry'('erased', 'erased', V3, V4, V5, V7)) end, ('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V6)))).

'un--keys'(V0, V1) -> ('erlang':'apply'('maps', 'keys', [('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V1)) | []])).

'un--insert'(V0, V1, V2, V3, V4, V5) -> ('erlang':'apply'('maps', 'put', [V3 | [V4 | [V5 | []]]])).

'un--get'(V0, V1, V2, V3, V4, V5) -> ('case--get-1371'('erased', 'erased', 'erased', V3, V5, V4, ('erlang':'apply'('maps', 'get', [V3 | [('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V4)) | []]])))).

'un--entries'(V0, V1) -> begin (V2 = ('erlang':'apply'('maps', 'to_list', [('Idris.Idris2.Builtin':'un--believe_me'('erased', 'erased', V1)) | []]))), ('Idris.Idris2.Prelude.Types':'dn--un--map_Functor__List'('erased', 'erased', fun (V3) -> case V3 of {E0, E1} -> (fun (V4, V5) -> {'Idris.Builtin.MkPair', V4, V5} end(E0, E1)); _ -> ('erlang':'throw'("Error: Unreachable branch")) end end, V2)) end.

'un--empty'() -> ('erlang':'apply'('maps', 'new', [])).

'un--delete'(V0, V1, V2, V3) -> ('erlang':'apply'('maps', 'remove', [V2 | [V3 | []]])).