From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 19 Nov 2015 15:40:50 +0000 (-0500)
Subject: indentation
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c6b822ac084a4472256bbccca2d4e1f2d289d48e;p=cubicaltt.git

indentation
---

diff --git a/Connections.hs b/Connections.hs
index 59aaee4..c1031ea 100644
--- 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 0ef2366..4e7a911 100644
--- 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)