Idris2 syntax for symbol types

Viewed 86

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?

0 Answers
Related