Pragmas

Idris2 supports a number of pragmas (identifiable by the % prefix). Some pragmas change compiler behavior until the behavior is changed back using the same pragma while others apply to the following declaration. A small niche of pragmas apply directly to one or more arguments instead of the code following the pragma (like the %name pragma described below).

Note

This page is a work in progress. If you know about a pragma that is not described yet, please consider submitting a pull request!

%builtin

The %builtin Natural pragma converts recursive/unary representations of natural numbers into primitive Integer representations.

This pragma is explained in detail on its own page. For more, see Builtins.

%deprecate

Mark the following definition as deprecated. Whenever the function is used, Idris will show a deprecation warning.

%deprecate
foo : String -> String
foo x = x ++ "!"

bar : String
bar = foo "hello"
Warning: Deprecation warning: Man.foo is deprecated and will be removed in a future version.

You can use code documentation (triple vertical bar ||| docs) to suggest a strategy for removing the deprecated function call and that documentation will be displayed alongside the warning.

||| Please use the @altFoo@ function from now on.
%deprecate
foo : String -> String
foo x = x ++ "!"

bar : String
bar = foo "hello"
Warning: Deprecation warning: Man.foo is deprecated and will be removed in a future version.
  Please use the @altFoo@ function from now on.

%inline

Instruct the compiler to inline the following definition when it is applied. It is generally best to let the compiler and the backend you are using optimize code based on its predetermined rules, but if you want to force a function to be inlined when it is called, this pragma will force it.

%inline
foo : String -> String
foo x = x ++ "!"

%noinline

Instruct the compiler _not_ to inline the following definition when it is applied. It is generally best to let the compiler and the backend you are using optimize code based on its predetermined rules, but if you want to force a function to never be inlined when it is called, this pragma will force it.

%noinline
foo : String -> String
foo x = x ++ "!"

%name

Give the compiler some suggested names to use for a particular type when it is asked to generate names for values. You can specify any number of suggested names; they will be used in-order when more than one is needed for a single definition.

data Foo = X | Y

%name Foo foo,bar