diff options
Diffstat (limited to 'src/Obs/Typing/Context.idr')
| -rw-r--r-- | src/Obs/Typing/Context.idr | 4 |
1 files changed, 2 insertions, 2 deletions
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)) |