Nuprl Definition : append
as @ bs == rec-case(as) of [] => bs | a::as' => r.[a / r]
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b]
Definitions occuring in definition :
list_ind: list_ind,
cons: [a / b]
Rules referencing :
barInduction
Latex:
as @ bs == rec-case(as) of [] => bs | a::as' => r.[a / r]
Date html generated:
2016_05_14-AM-06_28_13
Last ObjectModification:
2015_12_03-PM-02_05_12
Theory : list_0
Home
Index