WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites ptn
pr?
ptn_pr
Def ptn_pr(x) == inr(inr(inr(x)))
Thm*
T:Type, x:(T
T). ptn_pr(x)
ptn_con(T)
Thm*
x,y:Pattern. ptn_pr( < x,y > )
Pattern
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
T:Type, x:(T
T). ptn_pr(x) 
ptn_con(T)x,y:Pattern. ptn_pr( < x,y > ) PatternT:Type, x:(TT). ptn_pr(x) ptn_con(T)x,y:Pattern. ptn_pr( < x,y > ) Pattern
