When I opened the library, yesterday, even I had trouble finding the right imports at first (e.g., for compilers or expressiveness theorems). Moreover, the names of languages and atoms got really clumsy because I had to carry around annotation language F, the atom set equivalence, variant type around. To help myself, I created some aliases within the module I was using
|
STR : 𝔸 |
|
STR = (String , String._≟_) |
|
|
|
STRCCC = CCC String ∞ STR |
|
STR2CC = 2CC String ∞ STR |
|
STRADT = ADT (Rose ∞) String STR |
I think it would be great if we would have some helper modules to import all languages and compilers fixed to certain useful atom sets such as Strings (as used here) or natural numbers. Any other way of simplifying dealing with these names or imports is also ok.
Any other ideas?
When I opened the library, yesterday, even I had trouble finding the right imports at first (e.g., for compilers or expressiveness theorems). Moreover, the names of languages and atoms got really clumsy because I had to carry around annotation language F, the atom set equivalence, variant type around. To help myself, I created some aliases within the module I was using
Vatras/src/Vatras/Test/Experiments/ADT-to-TikZ-Forest.agda
Lines 22 to 27 in 81a5256
I think it would be great if we would have some helper modules to import all languages and compilers fixed to certain useful atom sets such as Strings (as used here) or natural numbers. Any other way of simplifying dealing with these names or imports is also ok.
Any other ideas?