This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next 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 133: | Line 133: | ||
| ''[[reference:subst|subst]]'' | a definition (or equation) | | x | x | ''subst (asm)'' | | | ''[[reference:subst|subst]]'' | a definition (or equation) | | x | x | ''subst (asm)'' | | ||
| ''[[reference:thin_tac|thin_tac]]'' | a formula | | | | | | | ''[[reference:thin_tac|thin_tac]]'' | a formula | | | | | | ||
- | | ''[[reference:unfold|unfold]]'' | a definition | x | x | ? | | | + | | ''[[reference:unfold|unfold]]'' | a definition (or equation) | x | x | ? | | |
=== Automated Methods === | === Automated Methods === | ||
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. |