From 67218e3eac55bd646b8e1e7074f72cd63a506905 Mon Sep 17 00:00:00 2001
From: "Thomas E. Hansen" <teh6@st-andrews.ac.uk>
Date: Mon, 5 Sep 2022 10:39:39 +0200
Subject: [PATCH] [ papers ] Move LTE' outside parameters block

---
 libs/papers/Search/CTL.idr | 32 +++++++++++++++-----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

diff --git a/libs/papers/Search/CTL.idr b/libs/papers/Search/CTL.idr
index 2206a3c94..2e0ddbc52 100644
--- a/libs/papers/Search/CTL.idr
+++ b/libs/papers/Search/CTL.idr
@@ -44,6 +44,21 @@ pComp (TD transFn1 iState1) (TD transFn2 iState2) =
                     map (\ (l1', st') => ((l1', l2), st')) (transFn1 (l1, st)) ++
                     map (\ (l2', st') => ((l1, l2'), st')) (transFn2 (l2, st)))
 
+-- different formulation of LTE, see also:
+-- https://agda.github.io/agda-stdlib/Data.Nat.Base.html#4636
+-- thanks @gallais!
+public export
+data LTE' : (n : Nat) -> (m : Nat) -> Type where
+  LTERefl : LTE' m m
+  LTEStep : LTE' n m -> LTE' n (S m)
+
+||| Convert LTE' to LTE
+lteAltToLTE : {m : _} -> LTE' n m -> LTE n m
+lteAltToLTE {m=0} LTERefl = LTEZero
+lteAltToLTE {m=(S k)} LTERefl = LTESucc (lteAltToLTE LTERefl)
+lteAltToLTE {m=(S m)} (LTEStep s) = lteSuccRight (lteAltToLTE s)
+
+
 parameters (Lbls, Sts : Type)
   ||| A computation tree (corecursive rose tree?)
   data CT : Type where
@@ -64,23 +79,6 @@ parameters (Lbls, Sts : Type)
       followAll [] = []
       followAll (st :: sts) = follow st :: followAll sts
       
-
-  -- different formulation of LTE, see also:
-  -- https://agda.github.io/agda-stdlib/Data.Nat.Base.html#4636
-  -- thanks @gallais!
-  public export
-  data LTE' : (n : Nat) -> (m : Nat) -> Type where
-    LTERefl : LTE' m m
-    LTEStep : LTE' n m -> LTE' n (S m)
-
-  ||| Convert LTE' to LTE
-  lteAltToLTE : {m : _} -> LTE' n m -> LTE n m
-  lteAltToLTE {m=0} LTERefl = LTEZero
-  lteAltToLTE {m=(S k)} LTERefl = LTESucc (lteAltToLTE LTERefl)
-  lteAltToLTE {m=(S m)} (LTEStep s) = lteSuccRight (lteAltToLTE s)
-
-  lteAltIsLTE : LTE' n m === LTE n m
-
   ||| A formula has a bound (for Bounded Model Checking; BMC) and a computation
   ||| tree to check against.
   public export