类库

这个编译指示告诉后端对一个给定的函数使用什么名字。

%nomangle
foo : Int -> Int
foo x = x + 1

在支持该功能的后端，该函数将被称为 foo 而不会被混淆，并带有命名空间。

如果您要使用的名称不是有效的 idris 标识符，则可以对已编译代码中显示的 idris 名称和函数使用不同的名称，例如。

%nomangle "$_baz"
baz : Int
baz = 42

你也可以为不同的后端指定不同的名称，类似于 %foreign 的方式

%nomangle "refc:idr_add_one"
          "node:add_one"
plusOne : Bits32 -> Bits32
plusOne x = x + 1