PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
reverse
T:Type, l:T*. ||l|| > 0
hd(rev(l)) = l[(||l||-1)]
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
l:
T*
3.
||l|| > 0
hd(rev(l)) = l[(||l||-1)]
About:
hd(rev(l)) = l[(||l||-1)] 
T:Type, l:T*. ||l|| > 0 
hd(rev(l)) = l[(||l||-1)] hd(rev(l)) = l[(||l||-1)]
