Idris2 syntax for symbol types

Question

In the Idris 1 documentation, 'foo is given as the syntax to create a symbol type: an empty type identified with its name:

Here, we have used a symbol type. In general ’name introduces a new symbol, the only purpose of which is to disambiguate values

The Idris 2 documentation on changes compared to Idris 1 doesn't mention symbol types at all, so that should suggest that they work as before. However, Idris2 chokes on symbol types with a parse error. For example:

public export
Html : Type -> Type
Html a = Node 'Html a

Couldn't parse declaration (next tokens: [identifier Html, identifier a, symbol =, identifier Node, Unrecognised ', identifier Html, identifier a, export, interface, identifier HtmlAllAttribute])

What is the new syntax for symbol types?

You could try making an issue on GitHub or asking on the Idris Slack — michaelmesser

Alissa Tung Alissa Tung · Accepted Answer · 2021-05-28T12:33:00

The syntax 'name simply introduces a new empty type, so locally define an empty type may help.

where
  data Foo : Type where

You can do some customary simplifications via elaborator reflection.

Idris2 syntax for symbol types

1 Answers