BoydStephenSmithJr, 7 months ago Does anyone have a #haskell or #agda GADT that models both general terms AND closed terms not containing any redex (values)? I seem to remember reading a random internet page with such a construction, but I can't remember enough for my Internet searching today to find it.
Does anyone have a #haskell or #agda GADT that models both general terms AND closed terms not containing any redex (values)?
I seem to remember reading a random internet page with such a construction, but I can't remember enough for my Internet searching today to find it.
Add comment