Closed application signatures shared by native evidence, artifact validation and host codecs. These are calling descriptors, not inferred erased IR types.
Closed application signatures shared by native evidence, artifact validation and host codecs. These are calling descriptors, not inferred erased IR types.
(arity signature)(display signature)(expected-type signature)Reconstruct the canonical closed Lean expression the producer must check by native DefEq. Argument names do not affect definitional equality.
Reconstruct the canonical closed Lean expression the producer must check by native DefEq. Argument names do not affect definitional equality.
(from-legacy profile)(runtime-arity signature)(validate! signature)Validate a bounded v2 JSON descriptor and return it unchanged. All arguments are explicit values; unsupported dependent/implicit/polymorphic binders must be rejected by the native classifier before issuing this descriptor.
Validate a bounded v2 JSON descriptor and return it unchanged. All arguments are explicit values; unsupported dependent/implicit/polymorphic binders must be rejected by the native classifier before issuing this descriptor.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |