T:Type, x:Atom. ptn_atom(x) 
ptn_con(T)x:Atom. ptn_atom(x) Patternx:Atom. ptn_atom(x) Label| Who Cites clbl? | |
| 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 | |
| Thm* x:Atom. ptn_atom(x) Label |
| Syntax: | $x | has structure: | clbl{$x:t} |
About:
 |  |  |  |  |  |  |