From 7e184c20d545afb55f6e962b8bfea882b23699fa Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 1 Jan 2023 12:11:50 +0000
Subject: Index normal forms with relevance.

- Remove container types.
- Replace sum types with booleans.
- Remove type annotation from absurd.
- Add original type as argument to cast.
- Make if (was case) take a lambda for the return type.
---
 src/Obs/Main.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Obs/Main.idr')

diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index fc7140a..4d7c856 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -54,7 +54,7 @@ main' : (input: String) -> Logging AnsiStyle (Exists NormalForm.Context)
 main' input = do
   defs <- parse input
   blk  <- abstractBlock defs
-  ctx  <- checkBlock blk
+  (_ ** (ctx, _)) <- checkBlock blk
   pure (Evidence _ ctx)
 
 partial
-- 
cgit v1.2.3