*+-: int or real /: real div: int mod: int binding: [1/a]
o : (’b -> ’c) * (’a -> ’b ) -> (’a -> ’c) map : ('a -> 'b) -> 'a list -> 'b list map map : ('a -> 'b) list -> ('a list -> 'b list) list fn L = > body List.filter : (’a -> bool) -> ’a list -> ’a list foldr : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b foldl : (’a * ’b -> ’b) -> ’b -> ’a list -> ’b
foldr (op ::) [] == id foldl (op ::) [] == rev
List.concat zip: (‘a list * ‘b list) -> (‘a * ‘b) list filter: ('a -> bool) -> 'a list -> 'a list inord: turn tree into list Fn.id
fun scal f z xs = foldl (fn (x, (last, acc)) => (f(x, last), f(x, last) :: acc)) (z, []) xs
(TODO: more)
Div Match Bind
For type: write out each sub component
fun f x = f x is 'a to 'b
fun f(x,y) = (f(x,y), f(x,y)) not well typed
Proof:
curry function argument valuable, like everything else
curry function totality only go through one level
write P(x) in IH
(see: https://piazza.com/class/kk66yt4thab5yx?cid=1808)
look at lemma constraints
Type
16:00 -> 17:15 -> 17:20
Functions!
Table of Content