diff options
| author | tslil <tslil@posteo.de> | 2026-05-06 14:27:43 +0100 |
|---|---|---|
| committer | tslil <tslil@posteo.de> | 2026-05-06 20:40:27 +0100 |
| commit | d682ad6bbb5547ffbcc19da90275ff43e4e03e20 (patch) | |
| tree | 43dc3bb60d0f65793e3a17fcf867ece0ff09ab8b /README.md | |
| parent | 1b4abb8fdd81f6de2166ef3f064a77fd5622fe83 (diff) | |
WiP
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -90,6 +90,10 @@ A construction admitting an instance of any signature, given an element of a var - **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]`. +### Notes + +There are no formal large eliminators, and as such we cannot perform case analysis on an element and produce varying set or signatures. However, the former construction may be losslessly encoded by detouring through instances-via-case-analysis and the signature `Set`. That is, `set-of(case m of [ ... | vi. xi => Xi :: Set | ... ])` is a set that varies depending on an element. + # License Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details. |