Changes

Directory:Jon Awbrey/Papers/Propositions As Types (view source)

Revision as of 19:34, 23 March 2009

144 bytes added , 19:34, 23 March 2009

→‎Step 2: markup

Line 34: Line 34:

===Step 2===

−

~~<pre>~~

+

Assign types in the following specification:

−

Assign types in the specification:

−

x_A = x_A ~~I_(~~A=>A)

+

{| align="center" cellpadding="8" width="90%"

+

| <math>x_A ~=~ x_A \operatorname{I}_{A \Rightarrow A}</math>

+

|}

−

~~to arrive at~~ a propositional typing for I : A => A,

+

A suitable type assignment provides a propositional typing for <math>\operatorname{I} : A \Rightarrow A,</math> whose type, read as a proposition, is a theorem of intuitionistic propositional calculus.

−

whose type, read as a proposition, is a theorem of

−

intuitionistic propositional calculus.

−

~~</pre>~~

===Step 3 (Optional)===

Jon Awbrey

12,140

edits