Little typer
- Normal forms
- Sameness according to a type
- 2 values the same <-> same normal form
- values the same if same constructor applied to the same values
- expression with constructor at top -> value
- constructors are the direct way of constructing expressions of that type
- value enough because the top-level ctor will dictate what happens next
- eliminators take apart values created by data constructors
- lambda is data ctor for functions