What does the %runElab directive do

[MakitaToki]

In the article Enum1.md, is the following code generated by the line %runElab (mkEnum "Gender"["Female","Male","NonBinary"]) ? I write the line %runElab (mkEnum "Gender"["Female","Male","NonBinary"]), but no changes happen.

export
Eq Gender where
  Female     == Female     = True
  Male       == Male       = True
  NonBinary  == NonBinary  = True
  _          == _          = False

[stefan-hoeck]

%runElab runs an elaborator script. In the above example, this results in a new data type called Gender with nullary constructors Male, Female, and NonBinary being defined. In order to make the changes visible, we implement an Eq instance for this new data type.

You can also try the following: Remove the line with %runElab from Enum1.md and try to typecheck the file. When Idris comes to the definition of Eq Gender, it will complain about no data type called Gender being in scope.

I updated Enum1.md with some clarifying remarks. Feel free to ask, if things remain unclear.

Here's a summary of the pieces interacting with each other:

• enumDecl: Returns a Decl: A syntax tree representing a declaration in Idris. When you write Idris code, Idris generates such declarations from your code. Here we generate some declarations programmatically.
• declare: Tells Idris to add a declaration to the local module / namespace of the call site. The result is of type Elab (): An elaborator script. Like an IO action, this needs some special way of being executed.
• %runElab: Executes an elaborator script. In our case, this generates a new data declaration as if we had manually written the corresponding data type in our source file.

[MakitaToki]

Thanks for your detailed explanation.