Module ErgoSpec.Backend.Qcert.QcertToJavascriptAst

Require Import Qcert.EJson.EJsonSystem.
Require Import Qcert.Translation.Operators.ForeignToJavaScriptAst.

Require Import QcertData.
Require Import QcertEJson.

Definition enhanced_ejson_to_ajavascript_expr (j:enhanced_ejson) : JsAst.JsSyntax.expr :=
  JsAst.JsSyntax.expr_literal (JsAst.JsSyntax.literal_null).

Instance enhanced_foreign_ejson_to_ajavascript :
  @foreign_ejson_to_ajavascript enhanced_foreign_ejson
  := mk_foreign_ejson_to_ajavascript
       enhanced_foreign_ejson
       enhanced_ejson_to_ajavascript_expr.