Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
primitive_notions_._wat [2015/12/17 20:28] nikolaj |
primitive_notions_._wat [2015/12/17 21:26] nikolaj |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| http://cstheory.stackexchange.com/questions/27400/minimal-specification-of-martin-l%C3%B6f-type-theory | http://cstheory.stackexchange.com/questions/27400/minimal-specification-of-martin-l%C3%B6f-type-theory | ||
| + | |||
| + | == Apple pie == | ||
| + | Think about what would be a good order of introduction (using WAT) (see [[Outline]]). | ||
| + | E.g. adding 5+3 would be among the very first things to do. | ||
| + | For educational purposes, talking about $\to, \times$ before more intricate concepts is also a good idea. | ||
| + | As I thought about before, going bottom top with the typy/computational/constructive stuff should be a good idea. Then, for sets and cats, it's the other other way around. | ||
| === Code === | === Code === | ||
