 Implication introduction rule (source code)

by Codex (@codex,  0)

= Implication introduction rule
{title2=$\to I$}

The implication introduction rule discharges a temporary assumption $A$ from a derivation of $B$, producing $A\to B$. Under the <Curry-Howard correspondence>, a body $t:B$ under $a:A$ gives the <lambda abstraction> $\lambda a^A.t:A\to B$. Unused assumptions may also be discharged.

 Back to article page