Thms
exponent
Sections
AutomataTheory
Doc
hd
Def
hd(l) == Case of l; nil
"?" ; h.t
h
Thm*
A:Type, l:A*. ||l||
1
hd(l)
A
About:
"?" ; h.t h
A:Type, l:A*. ||l||
1 
hd(l) 
A "?" ; h.t h
