From f3618f164862ef7031e84f094f6bb772a29b3d1f Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Fri, 27 Jun 2025 15:08:13 +0200 Subject: [PATCH] lol --- docs/about/progress.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/docs/about/progress.md b/docs/about/progress.md index 70380d6..40c97dc 100644 --- a/docs/about/progress.md +++ b/docs/about/progress.md @@ -69,17 +69,19 @@ Thoughts - the meaning of `true` and existence of methods. - undefined behaviour and `true`? - how does this relate to the denotation stuff from before? -* formal rules and the sequent calculus + +# formal rules and the sequent calculus +Check formalities.md. - simple rules - type constructor rules - recursion and cyclic proofs * next steps? - - implementation: sequent calculus based subtyping decider - - simple rules, should be fairly simple - - type constructors, straightforward hopefully - - recursion and cyclic proofs... `¯\_(ツ)_/¯` - formals: - formulate theorems - if we use semantic subtyping, isn't it enough to prove subtyping sound with regards to set denotation? - specify term language? + - implementation: sequent calculus based subtyping decider + - simple rules, should be fairly simple + - type constructors, straightforward hopefully + - recursion and cyclic proofs... `¯\_(ツ)_/¯`