Merge pull request #2838 from Melvar/show-funclause
Replace private Show FunClause with public one
commit5a38e0e1f67838b30abde8a2ed00bf7a764961f4
authorDavid Christiansen <david@davidchristiansen.dk>
dateWed 2 Dec 2015, 15:00 (11 years ago)
parentfe2dc3d0a6313d
libs/base/Language/Reflection/Utils.idr+4
@@ -349,3 +349,7 @@ 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 FunClause where
354+ showPrec d (MkFunClause lhs rhs) = showCon d "MkFunClause" $ showArg lhs ++
355+ showArg rhs
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 FunClause where
252− show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"
253−
254251abstract
255252deriveElim : (tyn, elimn : TTName) -> Elab ()
256253deriveElim tyn elimn =