From 6dd18d89bde30c9bdd3e6e0d198687dfd74aeeb1 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 22 Aug 2022 10:07:46 +0200 Subject: [PATCH] Uninhabited instances --- lib/Quox/Syntax/Qty.idr | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr index a9bdbd9..4ec000a 100644 --- a/lib/Quox/Syntax/Qty.idr +++ b/lib/Quox/Syntax/Qty.idr @@ -74,7 +74,11 @@ data IsSubj : Qty -> Type where SZero : IsSubj Zero SOne : IsSubj One +export Uninhabited (IsSubj Any) where uninhabited _ impossible + public export data IsGlobal : Qty -> Type where GZero : IsGlobal Zero GAny : IsGlobal Any + +export Uninhabited (IsGlobal One) where uninhabited _ impossible