Skip to content

Instantly share code, notes, and snippets.

@kikofernandez

kikofernandez/derivation.md

Created October 2, 2025 19:05
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save kikofernandez/a1e472cc83fe144c1e6571457cd708a1 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save kikofernandez/a1e472cc83fe144c1e6571457cd708a1 to your computer and use it in GitHub Desktop.
Download ZIP
Type derivation for mailbox typing
Raw
derivation.md
$$\cfrac{ \cfrac{ \frac{}{x \Leftarrow !m^{\circ} \blacktriangleright x:!m^\circ; \emptyset \qquad\qquad x:!m^\circ + . \blacktriangleright x:!m^\circ; \emptyset }} { \cfrac{ x!m[] \Rightarrow 1 \blacktriangleright x: !m^{\circ}; \emptyset \qquad 1 \leq 1 \blacktriangleright \emptyset } { x!m[] \Leftarrow 1 \blacktriangleright x: !m^{\circ}; \emptyset } } \qquad \qquad \cfrac{\text{new} \Leftarrow ?\boldsymbol{1}^\bullet \blacktriangleright .; \emptyset \qquad ?\boldsymbol{1}^\bullet \leq !m^\bullet} {\text{new} \Leftarrow !m^\bullet \blacktriangleright} }{ \text{let}\ x = \text{new in } x!m[] \Leftarrow 1 \blacktriangleright }$$
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment