@@ -1059,7 +1059,7 @@ elabPE info fc caller r =
1060 mkSpecialised ist specapp_in = do
1060 mkSpecialised ist specapp_in = do
1061 let (specTy, specapp) = getSpecTy ist specapp_in
1061 let (specTy, specapp) = getSpecTy ist specapp_in
1062− let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
1062+ let (n, newnm, pats) = getSpecClause ist specapp
1063 let undef = case lookupDef newnm (tt_ctxt ist) of
1063 let undef = case lookupDef newnm (tt_ctxt ist) of
1064 [] -> True
1064 [] -> True
1065 _ -> False
1065 _ -> False
@@ -1074,10 +1074,12 @@ elabPE info fc caller r =
1074 iLOG $ "PE definition type : " ++ (show specTy)
1074 iLOG $ "PE definition type : " ++ (show specTy)
1075 ++ "\n" ++ show opts
1075 ++ "\n" ++ show opts
1076 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
1076 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
1078+ (map (\ (lhs, rhs) ->
1077− (showImp Nothing True False lhs ++ " = " ++
1079+ (showImp Nothing True False lhs ++ " = " ++
1078− showImp Nothing True False rhs)
1080+ showImp Nothing True False rhs)) pats)
1079 elabType info defaultSyntax "" fc opts newnm specTy
1081 elabType info defaultSyntax "" fc opts newnm specTy
1080− let def = [PClause fc newnm lhs [] rhs []]
1082+ let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
1081 elabClauses info fc opts newnm def
1083 elabClauses info fc opts newnm def
1082 logLvl 1 $ "Specialised " ++ show newnm)
1084 logLvl 1 $ "Specialised " ++ show newnm)
1083 -- if it doesn't work, just don't specialise. Could happen for lots
1085 -- if it doesn't work, just don't specialise. Could happen for lots