Use fresh lists to enforce uniqueness of lexer keywords ?

[clayrat]

Fresh list is data structure defined by induction recursion for element types with a decidable equality.

Here's a PR to the Agda standard library with an implementation of fresh lists together with documentation & an updated version of the lexer example using fresh lists: agda/agda-stdlib#878

[gallais]

Note that it is crucial here to implement the generalised version of fresh lists that I have PR'd to the stdlib because we want to avoid duplicates not of pairs of string and token but of strings. So equality is not the freshness relation we are using here.

[clayrat]

There's an Idris implementation of fresh lists at https://github.com/ohad/collie/tree/main/src/Data/List