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