Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
product_type [2014/03/30 19:41] nikolaj |
product_type [2014/03/30 19:42] nikolaj |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| Depending on what we want to do with the type system, we might just replace expressions of computational equivalence $\rightsquigarrow$ by equality '$=$'. This symbol denotes a term rewriting, i.e. a computations alla | Depending on what we want to do with the type system, we might just replace expressions of computational equivalence $\rightsquigarrow$ by equality '$=$'. This symbol denotes a term rewriting, i.e. a computations alla | ||
| - | $\lambda x.\,\sin\,x\ \rightsquigarrow_\eta\ \sin,$ | + | $\left(\lambda x.\,3+x\right)\,4\ \rightsquigarrow_\beta\ 3+4,$ |
| or | or | ||
| - | $\left(\lambda x.\,3+x\right)\,4\ \rightsquigarrow_\beta\ 3+4.$ | + | $\lambda x.\,\sin\,x\ \rightsquigarrow_\eta\ \sin$ |
| ==== Parents ==== | ==== Parents ==== | ||
| === Related === | === Related === | ||
| [[Type theory]] | [[Type theory]] | ||
