mkName package:Agda

The Range sets the definition site of the name, not the use site.

Create a name from a string

Make a Name from some kind of string.

Create a name from a string. The boolean indicates whether a part of the name can be token constructor.