diff options
| -rw-r--r-- | README.md | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -86,7 +86,6 @@ For each `B ∈ { Nat, Int, Float, Str }`: - **η.** `I=for (x: X). I(x)` when x is not free in I. #### Instances via case analysis -A construction admitting an instance of any signature, given an element of a variant set and a branch for every tag. - **Intro.** `C ⊢ case m of [ v0. x0 => I0 | ... | vn. xn => In ] :: S` when `C ⊢ S signature`, `C ⊢ m : variant [ v0. : X0 | ... | vn. : Xn ]`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`. - **β.** `case vi. m of [ ... | vi. xi => Ii | ... ]=Ii[m/xi]`. |