Skip to content

Commit

Permalink
Merge pull request #28 from stefan-hoeck/constants
Browse files Browse the repository at this point in the history
[ fix ] constant data constructors use Con
  • Loading branch information
stefan-hoeck authored Mar 11, 2023
2 parents ac32552 + 74ef3bd commit 7f2697d
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions src/Text/Show/PrettyVal/Derive.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 7f2697d

Please sign in to comment.