From b2704dcbcc3a303e3224b7fffc242c1d595825d5 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Mon, 27 Jan 2025 22:45:18 -0500 Subject: [PATCH] Add getValues to JSON --- src/Parser/JSON.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index c71d95c..7baf9fa 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -122,6 +122,16 @@ getProperty prop (VObject xs) = Just (type ** (_, val)) => Just (type ** val) ``` +Return the values from an object. + +```idris +export +getValues : (object : JSONValue TObject) + -> (types : List JSONType ** DList JSONType JSONValue types) +getValues (VObject xs) = + dMap' (\t, (k, v) => (t ** v)) xs +``` + Recursively apply a filter to a JSON structure. ```idris