From 74ef3bd1ed1b96206d64b2eabebc30e5fc514859 Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Sat, 11 Mar 2023 16:23:24 +0100 Subject: [PATCH] [ fix ] constant data constructors use Con --- src/Text/Show/PrettyVal/Derive.idr | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Text/Show/PrettyVal/Derive.idr b/src/Text/Show/PrettyVal/Derive.idr index f0e7c13..187120e 100644 --- a/src/Text/Show/PrettyVal/Derive.idr +++ b/src/Text/Show/PrettyVal/Derive.idr @@ -15,10 +15,13 @@ import Derive.Prelude -- Utilities -------------------------------------------------------------------------------- --- Displays an applied constructer in record syntax. --- This is called, if all arguments have user-defined names. +||| Displays an applied constructer in record syntax. +||| This is called, if all arguments have user-defined names. +||| Note: If the list of arguments is empty, this uses the +||| `Con` data constructor in agreement with `parseValue`. public export rec : String -> List (Value,String) -> Value +rec con [] = Con (MkName con) [] rec con ps = Rec (MkName con) $ map (\(v,n) => (MkName n, v)) ps where named : Value -> String -> (VName,Value) named v name = (MkName name, v)