indentation

diff --git a/Connections.hs b/Connections.hs
index 59aaee494855d55d97dff4e9c5c523fdf7b2519d..c1031ea2abc7579601364598b3b2aeb281152433 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -254,6 +254,7 @@ propInvFormulaIncomp phi b = incomparables (invFormula phi b)
 -- testInvFormula = invFormula (Atom (Name 0) :/\: Atom (Name 1)) 1
 
 -- | Nominal
+
 -- gensym :: [Name] -> Name
 -- gensym xs = head (ys \\ xs)
 --   where ys = map Name $ ["i","j","k","l"] ++ map (('i':) . show) [0..]

diff --git a/Eval.hs b/Eval.hs
index 0ef236678e2e4ba67d33e8f98311d1f1b2431cbd..4e7a911391e8a3886ad0fdc83443a458f779f80a 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -202,9 +202,9 @@ app u v = case (u,v) of
     _ -> error $ "app: Split annotation not a Pi type " ++ show u
   (Ter Split{} _,_) | isNeutral v         -> VSplit u v
   (VComp (VPath i (VPi a f)) li0 ts,vi1) ->
-    let j   = fresh (u,vi1)
+    let j       = fresh (u,vi1)
         (aj,fj) = (a,f) `swap` (i,j)
-        tsj = Map.map (@@ j) ts
+        tsj     = Map.map (@@ j) ts
         v       = transFillNeg j aj vi1
         vi0     = transNeg j aj vi1
     in comp j (app fj v) (app li0 vi0)