} ]
[ { "{X | Γ ⊢ X : W}" * } {
class "wine" [
- [ "typed abstraction **" ] [ "Γ ⊢ λW" ]
+ [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ]
[ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
]
class "magenta" [
- [ "typed declaration ***" ] [ "Γ ⊢ pλW" ]
- [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+ [ "local typed declaration **" ] [ "Γ ⊢ -λW" ]
+ [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
]
class "prune" [
- [ "native type annotation *" ] [ "Γ ⊢ ⓣW" ]
+ [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+ ]
+ class "blue" [
+ [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ]
[ "no" ] [ "no" ] [ "yes" ] [ "no" ]
]
} ]
[ { "{X | Γ ⊢ X = V}" * } {
- class "blue" [
- [ "local abbreviation **" ] [ "Γ ⊢ δV" ]
+ class "sky" [
+ [ "local abbreviation *" ] [ "Γ ⊢ +δV" ]
[ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
]
- class "sky" [
- [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ]
+ class "cyan" [
+ [ "local definition **" ] [ "Γ ⊢ -δV" ]
+ [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ]
+ ]
+ class "water" [
+ [ "global definition ***" ] [ "Γ ⊢ pδV" ]
[ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
]
} ]
[ { "no" * } {
- class "cyan" [
+ class "green" [
[ "sort ****" ] [ "Γ ⊢ ⋆k" ]
[ "no" ] [ "no" ] [ "no" ] [ "no" ]
]
class "text" { 0 } { 2 * }
class "plane" { 1 }
-