\gdef\jdg#1{\:\mathrm{#1}}
\gdef\decode#1{\mathord{\uparrow}#1}
\gdef\code#1{\mathord{\downarrow}#1}
\gdef\jty{\:\mathrm{ty}}
\gdef\jprop{\:\mathrm{prop}}
\gdef\jtrue{\:\mathrm{true}}
\gdef\yields{\vdash}
\gdef\ms#1{\mathsf{#1}}
\gdef\mc#1{\mathcal{#1}}
\gdef\Open#1{{\Large \circ}{#1}}
\gdef\Close#1{{\Large \bullet}{#1}}
\gdef\OpenEta{\eta^{\circ}}
\gdef\CloseEta{\eta^{\bullet}}
\gdef\isStatic#1{\mathrm{isStatic}(#1)}
\gdef\isDynamic#1{\mathrm{isDynamic}(#1)}
\gdef\ite#1#2#3{\mathbf{if}\:\:#1\:\:\mathbf{then}\:\:#2\:\:\mathbf{else}\:\:#3}
\gdef\StOpn{{\Large \circ}_{\mathrm{st}}}
\gdef\Opn{{\Large \circ}}
\gdef\op{^\mathrm{op}}
\gdef\CC{\mathbb{C}}
Theory of Hippogriff
-
Flexible system for nominal things inspired by Narya
-
Universe of small types
-
Dependent record types
-
Pi types
-
Sum types
-
General recursion