T:Type, x:Atom. ptn_atom(x) 
ptn_con(T)x:Atom. ptn_atom(x) Pattern| No other cites to report in MarkB_generic | |
| clbl | Def $x == ptn_atom("$x") |
| ptn_atom | Def ptn_atom(x) == inl(x) |
| Thm* T:Type, x:Atom. ptn_atom(x) ptn_con(T) | |
| Thm* x:Atom. ptn_atom(x) Pattern |
| Syntax: | $x | has structure: | clbl{$x:t} |
About:
 |  |  |  |  |  |  |