Skip to content

Commit

Permalink
fix(12): use proper bracketing, don't use numeral
Browse files Browse the repository at this point in the history
Use zero instead of 0 to explicitly avoid notation here.
  • Loading branch information
spl authored and soonhokong committed Feb 4, 2016
1 parent 20a1403 commit 0acbf4e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion 12_Axioms.org
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ use of =Prop= entirely. Inductive types and Pi types can be viewed as
data types, and terms of these types can be "evaluated" by applying
reduction rules until no more rules can be applied. In principle, any
closed term (that is, term with no free variables) of type =ℕ= should
evaluate to a numeral, =succ (succ (succ ... 0))=.
evaluate to a numeral, =succ (... (succ zero)...)=.

Introducing a proof-irrelevant =Prop= and marking theorems irreducible
represents a first step towards separation of concerns. The intention
Expand Down

0 comments on commit 0acbf4e

Please sign in to comment.