Dear all,
I'm working on a small proof assistant in Haskell. In the logic that
I'm implementing it's very important that I distinguish between `large'
and `small' types for consistency reasons. I have worked to get this
distinction reflected in my types with the use of GADTs, like so:
data
On 16.03.11 10:26, Dominic Mulligan wrote:
Dear all,
I'm working on a small proof assistant in Haskell. In the logic that
I'm implementing it's very important that I distinguish between `large'
and `small' types for consistency reasons. I have worked to get this
distinction reflected in my
