User Tools
start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
start [2012/05/10 09:54] 131.246.92.39 [Methods] |
start [2012/07/19 14:59] 131.246.92.39 [Assorted gimmicks] |
||
|---|---|---|---|
| Line 217: | Line 217: | ||
| * ''f(x := y)'' -- the //function update//: the result of this expression is the function ''f'' updated such that it now returns ''y'' for parameter ''x''; the other values do not change. | * ''f(x := y)'' -- the //function update//: the result of this expression is the function ''f'' updated such that it now returns ''y'' for parameter ''x''; the other values do not change. | ||
| * ''{x. P x}'' -- the set of values fulfilling predicate ''P''. For instance, ''{x::nat. x dvd 125}'' is the set of (natural) divisors of $125$. | * ''{x. P x}'' -- the set of values fulfilling predicate ''P''. For instance, ''{x::nat. x dvd 125}'' is the set of (natural) divisors of $125$. | ||
| + | * ''{E x | x. P x}'' -- the set of values created by expression ''E'', for all values fulfilling predicate ''P'', ''{x + y | x y. x < 10 /\ y < 10}'' is the set of sums of all pairs of natural numbers with a single digit. | ||
start.txt · Last modified: 2014/04/30 15:28 by peter
Page Tools
