systemqfw

system Q F omega elaborator
git clone git://git.rr3.xyz/systemqfw
Log | Files | Refs | Submodules | README | LICENSE

commit 745159613779ccdbcf055e0013671030546ed489
parent b36eb6c5d887e88d250964a02d4d882050e349b8
Author: Robert Russell <robert@rr3.xyz>
Date:   Thu, 29 Aug 2024 15:49:30 -0700

Change how type definitions work

Don't bind variables; just assign names. This was how I did things
in DTLC, and it makes a lot of sense.

Diffstat:
MMain.hs | 3+--
1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Main.hs b/Main.hs @@ -293,8 +293,7 @@ declare typeCtx (Decl x k a) = do Left e -> print e *> exitFailure Right a -> pure a let a''' = V.evalType typeCtx.env a'' - let (lvl, typeCtx') = Ctx.bindAndAssign x' k' typeCtx - pure $ Ctx.define lvl a''' typeCtx' + pure $ Ctx.assign x' a''' k' typeCtx input :: Prog input =