From d682ad6bbb5547ffbcc19da90275ff43e4e03e20 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 6 May 2026 14:27:43 +0100 Subject: WiP --- README.md | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'README.md') diff --git a/README.md b/README.md index 1ff5a86..dedb96d 100644 --- a/README.md +++ b/README.md @@ -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. -- cgit v1.3.1