diff --git a/src/Parser/JSON.md b/src/Parser/JSON.md index 60386ef..35f6312 100644 --- a/src/Parser/JSON.md +++ b/src/Parser/JSON.md @@ -108,6 +108,18 @@ dFoldL f acc (VBool b) = f acc _ (VBool b) dFoldL f acc VNull = f acc _ VNull ``` +Look up a property in an object + +```idris +export +getProperty : (prop : String) -> (object : JSONValue TObject) + -> Maybe (type : JSONType ** JSONValue type) +getProperty prop (VObject xs) = + case dFind (\_, (key, _) => key == prop) xs of + Nothing => Nothing + Just (type ** (_, val)) => Just (type ** val) +``` + ## Parsers We are going to get mutually recursive here. Instead of using a `mutual` block,