doc-src/Logics/HOL.tex
changeset 3881 73be08b4da3f
parent 3489 afa802078173
child 3959 033633d9a032
equal deleted inserted replaced
3880:d93c62ec97a6 3881:73be08b4da3f
  1247   \tt \#   & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & 
  1247   \tt \#   & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & 
  1248         list constructor \\
  1248         list constructor \\
  1249   \cdx{null}    & $\alpha\,list \To bool$ & & emptiness test\\
  1249   \cdx{null}    & $\alpha\,list \To bool$ & & emptiness test\\
  1250   \cdx{hd}      & $\alpha\,list \To \alpha$ & & head \\
  1250   \cdx{hd}      & $\alpha\,list \To \alpha$ & & head \\
  1251   \cdx{tl}      & $\alpha\,list \To \alpha\,list$ & & tail \\
  1251   \cdx{tl}      & $\alpha\,list \To \alpha\,list$ & & tail \\
  1252   \cdx{ttl}     & $\alpha\,list \To \alpha\,list$ & & total tail \\
  1252   \cdx{last}    & $\alpha\,list \To \alpha$ & & last element \\
       
  1253   \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
  1253   \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
  1254   \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
  1254   \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
  1255   \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
  1255         & & apply to all\\
  1256         & & apply to all\\
  1256   \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
  1257   \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
  1257         & & filter functional\\
  1258         & & filter functional\\
  1291 null [] = True
  1292 null [] = True
  1292 null (x#xs) = False
  1293 null (x#xs) = False
  1293 
  1294 
  1294 hd (x#xs) = x
  1295 hd (x#xs) = x
  1295 tl (x#xs) = xs
  1296 tl (x#xs) = xs
       
  1297 tl [] = []
  1296 
  1298 
  1297 [] @ ys = ys
  1299 [] @ ys = ys
  1298 (x#xs) @ ys = x # xs @ ys
  1300 (x#xs) @ ys = x # xs @ ys
  1299 
  1301 
  1300 map f [] = []
  1302 map f [] = []