diff options
| author | tslil <tslil@posteo.de> | 2026-05-07 17:27:17 +0100 |
|---|---|---|
| committer | tslil <tslil@posteo.de> | 2026-05-07 17:27:19 +0100 |
| commit | 55ea9c739c8e42df0caf8a3394add7bd7931a189 (patch) | |
| tree | d5eec34c7828275f5a08e4778ffa8aa6d760fe49 /README.md | |
| parent | ac0694074630f1308e44e42eb9bf0d228460fbf1 (diff) | |
remove stray sentence
Diffstat (limited to 'README.md')
| -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]`. |