From 49e4b61cd6b8150e516997606e803bfeec75d1f0 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 18 Dec 2022 22:56:48 +0000 Subject: Add dependent sums. --- src/Obs/Abstract.idr | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/Obs/Abstract.idr') 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) -- cgit v1.2.3