MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / from_json_strings

Method from_json_strings

lean_py/registry.py:189–222  ·  view source on GitHub ↗
(cls, funcs_json: str, types_json: str)

Source from the content-addressed store, hash-verified

187 if k == "string":
188 return isinstance(value, str)
189 if k == "pyobject":
190 return True
191 if k in ("array", "list"):
192 if not isinstance(value, (list, tuple)):
193 return False
194 return self.elem is None or all(self.elem.matches(v) for v in value)
195 if k == "option":
196 return value is None or (self.elem is not None and self.elem.matches(value))
197 if k == "prod":
198 return (
199 isinstance(value, tuple)
200 and len(value) == 2
201 and self.a is not None
202 and self.a.matches(value[0])
203 and self.b is not None
204 and self.b.matches(value[1])
205 )
206 if k == "sum":
207 return (self.a is not None and self.a.matches(value)) or (
208 self.b is not None and self.b.matches(value)
209 )
210 if k == "io":
211 return self.elem is None or self.elem.matches(value)
212 if k == "except":
213 return self.a is None or self.a.matches(value)
214 if k in ("named", "opaque"):
215 return self._matches_named(value)
216 return True
217
218 def _matches_named(self, value: Any) -> bool:
219 # A Lean inductive value/constructor carries its own type name; if so,
220 # require it to match. Anything else (tuple spellings, opaque handles)
221 # is accepted leniently.
222 type_name = getattr(value, "_type_name", None)
223 if type_name is None:
224 type_name = getattr(type(value), "_type_name", None)
225 if type_name is None:

Callers 1

_load_registryMethod · 0.80

Calls 2

from_jsonMethod · 0.45
addMethod · 0.45

Tested by

no test coverage detected