From cb4ec1e7c1551c1d28f00ba11b062daa78e8c4e3 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 20 Dec 2022 11:07:04 +0000 Subject: Add equality types and casts. --- src/Obs/Abstract.idr | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) (limited to 'src/Obs/Abstract.idr') diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr index ef90cb8..9215dda 100644 --- a/src/Obs/Abstract.idr +++ b/src/Obs/Abstract.idr @@ -57,6 +57,28 @@ abstractSyntax ctx (Absurd bounds a t) = do a <- abstractSyntax ctx a t <- abstractSyntax ctx t pure (Absurd bounds a t) +abstractSyntax ctx (Equal bounds t u) = do + t <- abstractSyntax ctx t + u <- abstractSyntax ctx u + pure (Equal bounds t u) +abstractSyntax ctx (Refl bounds t) = do + t <- abstractSyntax ctx t + pure (Refl bounds t) +abstractSyntax ctx (Transp bounds t b u t' e) = do + t <- abstractSyntax ctx t + b <- abstractSyntax ctx b + u <- abstractSyntax ctx u + t' <- abstractSyntax ctx t' + e <- abstractSyntax ctx e + pure (Transp bounds t b u t' e) +abstractSyntax ctx (Cast bounds b e t) = do + b <- abstractSyntax ctx b + e <- abstractSyntax ctx e + t <- abstractSyntax ctx t + pure (Cast bounds b e t) +abstractSyntax ctx (CastId bounds t) = do + t <- abstractSyntax ctx t + pure (CastId bounds t) abstractDefinition : Context n -> Definition -> Logging ann (Definition n) abstractDefinition ctx def = pure $ MkDefinition -- cgit v1.2.3