From 85f20680e6382895fb90dad37e7cb3d8f94c1653 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 23 May 2024 23:28:43 +0200 Subject: [PATCH] add constructors to Located/Relocatable interfaces --- lib/Quox/Loc.idr | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/lib/Quox/Loc.idr b/lib/Quox/Loc.idr index fae1bf8..5e25d13 100644 --- a/lib/Quox/Loc.idr +++ b/lib/Quox/Loc.idr @@ -125,7 +125,9 @@ extendOr l1 l2 = (l1 `extendL` l2) `or` l2 public export -interface Located a where (.loc) : a -> Loc +interface Located a where + constructor MkLocated + (.loc) : a -> Loc public export 0 Located1 : (a -> Type) -> Type @@ -136,7 +138,10 @@ public export Located2 f = forall x, y. Located (f x y) public export -interface Located a => Relocatable a where setLoc : Loc -> a -> a +public export +interface Located a => Relocatable a where + constructor MkRelocatable + setLoc : Loc -> a -> a public export 0 Relocatable1 : (a -> Type) -> Type