search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

add basic json accessors #1322

Closed rsoeldner closed 1 month ago

rsoeldner commented 1 month ago

add basic functionality for working with json @konrad-slind, what do you think?

konrad-slind commented 1 month ago

Looks good. A couple of comments:

  1. foldArray isn't really a fold. It's doing a map of f across the array (actually a list) and then revealing the resulting list. So I am not quite sure what to call the entry point.

  2. We could think about changing the Json.sig file to make the json type abstract. Would then need an entry point isNull.