Make implicit variables accessible for proofs.

1 files changed, 15 insertions, 15 deletions

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 9e1ef91..50b65e0 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -36,7 +36,7 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
   constructor MkIsAlgebra
   equivalence : IEquivalence (uncurry a.U) rel
   -- Congruences
-  renameCong  : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
+  renameCong  : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
     -> {tm, tm' : a.U t ctx} -> rel (t, ctx) tm tm'
     -> rel (t, ctx') (a.rename t f tm) (a.rename t f tm')
   semCong     : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
@@ -44,18 +44,18 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
     -> Pointwise (extendRel {U = a.U} rel ctx) tms tms'
     -> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
   substCong   : (t : sig.T) -> (ctx : List sig.T)
-    -> forall ctx' . {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm'
+    -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm'
     -> {tms, tms' : (\t => a.U t ctx) ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms'
     -> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
   -- rename is functorial
   renameId    : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
     -> rel (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
-  renameComp  : (t : sig.T)
-    -> forall ctx, ctx', ctx'' . (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx')
+  renameComp  : (t : sig.T) -> {ctx, ctx', ctx'' : _}
+    -> (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx')
     -> (tm : a.U t ctx)
     -> rel (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
   -- sem are natural transformation
-  semNat      : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
+  semNat      : {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.U ctx ^ op.arity)
     -> rel (t, ctx')
          (a.rename t f $ a.sem ctx op tms)
@@ -63,34 +63,34 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
           map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $
           tms)
   -- var is natural transformation
-  varNat      : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
+  varNat      : {t : _} -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
     -> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
   -- subst is natural transformation
-  substNat    : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
-    -> forall ctx'' . (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx) ^ ctx'')
+  substNat    : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
+    -> {ctx'' : _} -> (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx) ^ ctx'')
     -> rel (t, ctx')
          (a.rename t f $ a.subst t ctx tm tms)
          (a.subst t ctx' tm $ map (\t => a.rename t f) tms)
   -- subst is extranatural transformation
   substExnat  : (t : sig.T) -> (ctx : List sig.T)
-    -> forall ctx', ctx'' . (f : ctx' `Sublist` ctx'')
+    -> {ctx', ctx'' : _} -> (f : ctx' `Sublist` ctx'')
     -> (tm : a.U t ctx') -> (tms : (\t => a.U t ctx) ^ ctx'')
     -> rel (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms))
   -- var, subst is a monoid
   substComm   : (t : sig.T) -> (ctx : List sig.T)
-    -> forall ctx', ctx'' . (tm : a.U t ctx'')
+    -> {ctx', ctx'' : _} -> (tm : a.U t ctx'')
     -> (tms : (\t => a.U t ctx') ^ ctx'') -> (tms' : (\t => a.U t ctx) ^ ctx')
     -> rel (t, ctx)
          (a.subst t ctx (a.subst t ctx' tm tms) tms')
          (a.subst t ctx tm $ map (\t, tm => a.subst t ctx tm tms') tms)
-  substVarL   : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx')
+  substVarL   : {t : _} -> (ctx : List sig.T) -> {ctx' : _} -> (i : Elem t ctx')
     -> (tms : (\t => a.U t ctx) ^ ctx')
     -> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
   substVarR   : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
     -> rel (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
   -- sem, var and subst are compatible
   substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-    -> forall ctx' . (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx')
+    -> {ctx' : _} -> (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx')
     -> rel (t, ctx)
          (a.subst t ctx (a.sem ctx' op tms) tms')
          (a.sem ctx op $
@@ -132,16 +132,16 @@ record IsHomomorphism
   constructor MkIsHomomorphism
   cong       : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
     -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (f t ctx tm) (f t ctx tm')
-  renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
+  renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
     -> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
   semHomo    : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.raw.U ctx ^ op.arity)
     -> b.relation (t, ctx)
          (f t ctx $ a.raw.sem ctx op tms)
          (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
-  varHomo    : forall t, ctx . (i : Elem t ctx)
+  varHomo    : {t : _} -> {ctx : _} -> (i : Elem t ctx)
     -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
-  substHomo  : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx')
+  substHomo  : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
     -> (tms : (\t => a.raw.U t ctx) ^ ctx')
     -> b.relation (t, ctx)
          (f t ctx $ a.raw.subst t ctx tm tms)