Is it currently possible to formulate: "Let
A be a type/term for which 'param1' has been derived"?
In my definition of "expression of a programming language" I wanted to abstract over the type of identifier used. Its not necessary, but would have been nice.
In that casa you should take 2 parameters, A and PA : A -> Type.
Last updated: Feb 05 2023 at 15:03 UTC