Differences

This shows you the differences between two versions of the page.

--- sav08:syntax_and_shorthands_of_hol [2008/05/28 01:04]
vkuncak
+++ sav08:syntax_and_shorthands_of_hol [2008/05/28 02:58]
vkuncak
@@ Line 31: / Line 31: @@
 \lnot F & (F = false) \\
 F_1 \land F_2 & (\lambda g.\ g\ true\ true) = (\lambda g.\ F_1\ F_2) \\
-\forall x_{t_1}. F_{t_2} &  (\lambda x. F) = (\lambda x. true) \\
+\forall x. F &  (\lambda x. F) = (\lambda x. true) \\
 \end{array}
 \]
 Note that we have defined negation, conjunction, and universal quantification, so all propositional operations and existential quantification are expressible.
+Note also that we can express
+\[
+   \mbox{ let } x = E \mbox{ in } F
+\]
+by $(\lambda x.F)E$.
+The selection operator $\iota$ is not essential, but is a useful notation.  By writing
+\[
+   \mbox{ let } y = \iota(\lambda x. P(x)) \mbox{ in } F
+\]
+we can express the phrase "let y in F denote the unique x such that P(x) holds".