diff options
Diffstat (limited to 'src/Obs/Abstract.idr')
| -rw-r--r-- | src/Obs/Abstract.idr | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr index 90616d4..ef90cb8 100644 --- a/src/Obs/Abstract.idr +++ b/src/Obs/Abstract.idr @@ -36,6 +36,20 @@ abstractSyntax ctx (App t u) = do t <- abstractSyntax ctx t u <- abstractSyntax ctx u pure (App t u) +abstractSyntax ctx (Sigma bounds var a b) = do + a <- abstractSyntax ctx a + b <- abstractSyntax (bind ctx var.val) b + pure (Sigma bounds var.val a b) +abstractSyntax ctx (Pair b t u) = do + t <- abstractSyntax ctx t + u <- abstractSyntax ctx u + pure (Pair b t u) +abstractSyntax ctx (Fst b t) = do + t <- abstractSyntax ctx t + pure (Fst b t) +abstractSyntax ctx (Snd b t) = do + t <- abstractSyntax ctx t + pure (Snd b t) abstractSyntax ctx (Top b) = pure (Top b) abstractSyntax ctx (Point b) = pure (Point b) abstractSyntax ctx (Bottom b) = pure (Bottom b) |