-
Notifications
You must be signed in to change notification settings - Fork 21
Open
Description
lean has implemented_by https://github.com/leanprover/lean4/blob/1f9bba9d398e207ebbb62696b84502ad764d39dc/src/Init/Data/Array/Basic.lean#L533
and I would like to implement optimizations like this purescript/purescript-json#9
proposal
module PureScript.Backend.Optimizer.Directives.Defaults where
defaultDirectives :: String
defaultDirectives =
"""
...
JSON.fromBoolean implemented_by unsafeCoerce
JSON.fromInt implemented_by unsafeCoerce
JSON.fromString implemented_by unsafeCoerce
JSON.fromJArray implemented_by unsafeCoerce
JSON.fromJObject implemented_by unsafeCoerce
JSON.Array.signleton implemented_by unsafeCoerce [unsafeCoerce x]
JSON.Internals.toArray implemented_by unsafeCoerce
JSON.Internals.fromArray implemented_by unsafeCoerce
JSON.Internals.empty implemented_by unsafeCoerce []
"""Alternative - implement js backend for lean :)
Metadata
Metadata
Assignees
Labels
No labels