Merge remote-tracking branch 'upstream/master' into shlevy-elab-lookup-function-def
commitfe3b1a396e70c67d5429b46cb0d660791366461c
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateWed 2 Dec 2015, 20:50 (11 years ago)
parent3edbd8e5a38e0e
libs/base/Language/Reflection/Utils.idr+6
@@ -349,3 +349,9 @@ instance Show CtorArg where
349349instance Show TyDecl where
350350 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++
351351 showArg args ++ showArg ret
352+
353+instance Show tm => Show (FunClause tm) where
354+ showPrec d (MkFunClause lhs rhs) =
355+ showCon d "MkFunClause" $ showArg lhs ++ showArg rhs
356+ showPrec d (MkImpossibleClause lhs) =
357+ showCon d "MkImpossibleClause" $ showArg lhs
libs/pruviloj/Pruviloj/Derive/Eliminators.idr−3
@@ -248,9 +248,6 @@ getElimClauses info elimn ctors =
248248 in traverse (\(i, con) => getElimClause info elimn methodCount con i)
249249 (enumerate ctors)
250250
251−instance (Show a) => Show (FunClause a) where
252− show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"
253−
254251abstract
255252deriveElim : (tyn, elimn : TTName) -> Elab ()
256253deriveElim tyn elimn =