Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have added details to product type on both positive and negative definitions, with the corresponding beta and eta reduction rules.
Also stubs at positive type and negative type.
And a bit of similar detail at sum type.
Nice! I’ve been thinking about denotational semantics lately, where the distinction between positive and negative types corresponds to eager vs lazy evaluation, so I put in some notes about that, but so far they link to nothing.
I was wondering about that a while back and checking now with Google… yes, the first hit for “negative type” is Type O Negative :-)
replaced the old product natural deduction - table with a better typeset version (here)
1 to 7 of 7