-
Francesco Mazzoli authored
Note that now interaction with Agda is getting more complicated -- `open import Prelude` is interpreted by `tog`. Moreover, I don't want to make an effort in mimicking the record behaviour, since we're probably going to change it anyway. Note that the released `bnfc` is buggy, and the git `bnfc` is buggy, so while <https://github.com/BNFC/bnfc/pull/116> gets merged you need my version of `bnfc`: <https://github.com/BNFC/bnfc/pull/116>.
175730b9