lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

List.md (341B)

      1 +++
      2 title = "List"
      3 +++
      4 
      5 # List
      6 a list is made by repeatedly forming a pair:
      7 `[1,2,3]` is `(1, (2, (3, nil) ) )`
      8 
      9 **definition**
     10 - constructor for empty list:
     11 	- nil := λxy.y
     12 - constructor for cons:
     13 	- cons := λht.λz.z h t
     14 
     15 then:
     16 - nil = λxy.y
     17 - cons H T =β λz.z H T
     18 
     19 **head and tail**
     20 - head := λl.l (λht.h)
     21 - tail := λl.l (λht.t)