WhoCites
Definitions
mb
declaration
Sections
GenAutomata
Doc
Who Cites hd?
hd
Def hd(l) == Case of l; nil
"?" ; h.t
h
Thm*
A:Type, l:A List. ||l||
1
hd(l)
A
Thm*
A:Type, l:A List
. hd(l)
A
About:
WhoCites
Definitions
mb
declaration
Sections
GenAutomata
Doc
"?" ; h.t h
A:Type, l:A List. ||l||
1 
hd(l) 
AA:Type, l:A List
. hd(l) A "?" ; h.t hA:Type, l:A List. ||l||1 hd(l) AA:Type, l:A List. hd(l) A
