From 0608a7abedf738215560865e43d50909c1652c18 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 16 Oct 2008 13:30:40 -0400 Subject: Improving indentation of XML after antiquote --- lib/top.ur | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/top.ur b/lib/top.ur index 1b1d1ec5..4b9f54ef 100644 --- a/lib/top.ur +++ b/lib/top.ur @@ -34,10 +34,10 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) (fn _ => i) fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = + (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) [[nm] ~ rest] r => @@ -45,10 +45,10 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) (fn _ => i) fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = + (f : nm :: Name -> t :: Type -> rest :: {Type} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => -- cgit v1.2.3