From c653fcb664071dc4e644c8396e312daf3a89673c Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 27 Feb 2022 01:49:42 +0100 Subject: [PATCH] more formatting stuff --- src/Quox/Syntax/Var.idr | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr index b71dba5..7f52766 100644 --- a/src/Quox/Syntax/Var.idr +++ b/src/Quox/Syntax/Var.idr @@ -194,20 +194,20 @@ data LTE : Var n -> Var n -> Type where export Reflexive (Var n) LTE where reflexive {x = VZ} = LTEZ - reflexive {x = VS i} = LTES $ reflexive {x=i} + reflexive {x = VS i} = LTES $ reflexive {x = i} export Transitive (Var n) LTE where transitive LTEZ q = LTEZ - transitive (LTES p) (LTES q) = LTES $ transitive p q {rel=Var.LTE} + transitive (LTES p) (LTES q) = LTES $ transitive p q {rel = Var.LTE} export Antisymmetric (Var n) LTE where antisymmetric LTEZ LTEZ = Refl - antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel=Var.LTE} + antisymmetric (LTES p) (LTES q) = cong VS $ antisymmetric p q {rel = Var.LTE} export -splitLTE : {j : Var n} -> i `Var.LTE` j -> Either (i = j) (i `Var.LT` j) +splitLTE : {j : Var n} -> i `LTE` j -> Either (i = j) (i `LT` j) splitLTE {j = VZ} LTEZ = Left Refl splitLTE {j = VS _} LTEZ = Right LTZ splitLTE (LTES p) with (splitLTE p)