0 | module Idris.Syntax.Builtin
 1 |
 2 | import Core.Name
 3 |
 4 | %default total
 5 |
 6 | export
 7 | pairname : Name
 8 | pairname = NS builtinNS (UN $ Basic "Pair")
 9 |
10 | export
11 | mkpairname : Name
12 | mkpairname = NS builtinNS (UN $ Basic "MkPair")
13 |
14 | export
15 | dpairname : Name
16 | dpairname = NS dpairNS (UN $ Basic "DPair")
17 |
18 | export
19 | mkdpairname : Name
20 | mkdpairname = NS dpairNS (UN $ Basic "MkDPair")
21 |
22 | export
23 | nilName : Name
24 | nilName = NS preludeNS (UN $ Basic "Nil")
25 |
26 | export
27 | consName : Name
28 | consName = NS preludeNS (UN $ Basic "::")
29 |
30 | export
31 | interpolateName : Name
32 | interpolateName = NS preludeNS (UN $ Basic "interpolate")
33 |
34 | export
35 | eqName : Name
36 | eqName = NS builtinNS (UN $ Basic "===")
37 |
38 | export
39 | heqName : Name
40 | heqName = NS builtinNS (UN $ Basic "~=~")
41 |