From e8a5ba7c22c98d32671d02e41960598566bdcc58 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 5 Dec 2022 14:37:30 +0000
Subject: WIP: port to library

---
 src/Syntax/PreorderReasoning/Setoid.idr | 55 ---------------------------------
 1 file changed, 55 deletions(-)
 delete mode 100644 src/Syntax/PreorderReasoning/Setoid.idr

(limited to 'src/Syntax/PreorderReasoning/Setoid.idr')

diff --git a/src/Syntax/PreorderReasoning/Setoid.idr b/src/Syntax/PreorderReasoning/Setoid.idr
deleted file mode 100644
index f0480b2..0000000
--- a/src/Syntax/PreorderReasoning/Setoid.idr
+++ /dev/null
@@ -1,55 +0,0 @@
-{- Taken from https://github.com/ohad/idris-setoid -}
-
-||| Like Syntax.PreorderReasoning.Generic, but optimised for setoids
-module Syntax.PreorderReasoning.Setoid
-
-import public Data.Setoid
-
-infixl 0  ~~
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
-
-public export
-data Step : (a : Setoid) -> (lhs,rhs : U a) -> Type where
-  (...) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
-    a.relation x y -> Step a x y
-
-public export
-data FastDerivation : (a : Setoid) -> (x, y : U a) -> Type where
-  (|~) : {0 a : Setoid} -> (x : U a) -> FastDerivation a x x
-  (~~) : {0 a : Setoid} -> {x, y : U a}
-         -> FastDerivation a x y -> {z : U a} -> (step : Step a y z)
-         -> FastDerivation a x z
-
-public export
-CalcWith : (a : Setoid) -> {0 x : U a} -> {0 y : U a} -> FastDerivation a x y ->
-  a.relation x y
-CalcWith a (|~ x) = a.equivalence.reflexive
-CalcWith a ((~~) der (z ... step)) = a.equivalence.transitive
-    (CalcWith a der) step
-
--- Smart constructors
-public export
-(..<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
-    a.relation y x -> Step a x y
-(y ..<(prf)) {x} = (y ...(a.equivalence.symmetric prf))
-
-public export
-(..>) : {0 a : Setoid} -> (0 y : U a) -> {0 x : U a} ->
-    a.relation x y -> Step a x y
-(..>) = (...)
-
-public export
-(.=.) : {a : Setoid} -> (y : U a) -> {x : U a} ->
-    x === y -> Step a x y
-(y .=.(Refl)) = (y ...(a.equivalence.reflexive))
-
-public export
-(.=>) : {a : Setoid} -> (y : U a) -> {x : U a} ->
-    x === y -> Step a x y
-(.=>) = (.=.)
-
-public export
-(.=<) : {a : Setoid} -> (y : U a) -> {x : U a} ->
-    y === x -> Step a x y
-(y .=<(Refl)) = (y ...(a.equivalence.reflexive))
-- 
cgit v1.2.3