diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-10-16 13:30:40 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-16 13:30:40 -0400 |
commit | 0608a7abedf738215560865e43d50909c1652c18 (patch) | |
tree | 302c9cf9d9eb49b3cd90978b8ff1b18393d0c2e3 /lib | |
parent | 98c2a658375be784ec9afaa80146e5dff3514e5c (diff) |
Improving indentation of XML after antiquote
Diffstat (limited to 'lib')
-rw-r--r-- | lib/top.ur | 16 |
1 files changed, 8 insertions, 8 deletions
@@ -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 => |