From 06bd13433cb5e7edcff551454107c9d4e4d88f8f Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Thu, 5 Jan 2023 17:06:33 +0000 Subject: Add more program structure to normal forms. --- src/Obs/Typing/Context.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Obs/Typing/Context.idr') diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr index 4706dca..ad1d0a7 100644 --- a/src/Obs/Typing/Context.idr +++ b/src/Obs/Typing/Context.idr @@ -64,7 +64,7 @@ fromVar var = MkDefinition { name = var.name , sort = var.sort , ty = weaken [relevance var.sort] var.ty - , tm = point (var.name, (var.sort ** Refl)) Here + , tm = point (Just var.name) Here , correct = Refl } @@ -104,5 +104,5 @@ reduce : (tyCtx : TyContext ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx) reduce [] = absurd reduce (ctx :< def) = add (LogNormalForm ann) (subst def.tm (reduce ctx)) (reduce ctx) reduce (ctx ::< var) = add (LogNormalForm ann) - (pure $ point (var.name, (var.sort ** Refl)) Here) + (pure $ point (Just var.name) Here) (\i => pure $ weaken [_] $ !(reduce ctx i)) -- cgit v1.2.3