From 224c59ec520c92ed9e7e1d4e228e3c53acdff61e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 24 May 2023 15:48:28 +0100
Subject: Give a defunctionalised fuel-powered interpreter.

---
 src/NormalForm.idr | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/NormalForm.idr')

diff --git a/src/NormalForm.idr b/src/NormalForm.idr
index f4697f5..ea3b2c0 100644
--- a/src/NormalForm.idr
+++ b/src/NormalForm.idr
@@ -35,6 +35,9 @@ record Normal (ctx : SnocList Ty) (ty : Ty) where
 
 -- Inversions ------------------------------------------------------------------
 
+export
+Uninhabited (IsNormal (Sub t sub)) where uninhabited (Ntrl prf) impossible
+
 export
 predNorm : IsNormal (Succ t) -> IsNormal t
 predNorm (Succ prf) = prf
-- 
cgit v1.2.3