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.
at implication there is currently the statement
$q \to r \vdash (p \to q) \to (q \to r)$,
That’s a typo, right?
Well, it’s correct, though probably $q \to r \vdash (p \to q) \to (p \to r)$ is meant.
I made that typo; and worse, I seem to have consistently reversed syntax and semantics! Fixed.
I have edited implication a little bit, making the definition section point to hypothetical judgement where it discusses entailment, and adding a brief remark towards the end on the relation to function types.
1 to 4 of 4