x,y:Pattern. lbl_pr( < x, y > ) 
PatternT:Type, x:(T
T). ptn_pr(x) ptn_con(T)x,y:Pattern. ptn_pr( < x,y > ) Pattern| No other cites to report in MarkB_generic | |
| lbl_pair | Def lbl_pr( < x, y > ) == ptn_pr( < x,y > ) |
| Thm* x,y:Pattern. lbl_pr( < x, y > ) Pattern | |
| ptn_pr | Def ptn_pr(x) == inr(inr(inr(x))) |
| Thm* T:Type, x:(TT). ptn_pr(x) ptn_con(T) | |
| Thm* x,y:Pattern. ptn_pr( < x,y > ) Pattern |
| Syntax: | lbl_pr( < x, y > ) | has structure: | lbl_pair(x; y) |
About:
 |  |  |  |  |  |  |