module Spartan6.Unsafe.Examples.GeneratedJson where

open import Cubical.Foundations.Prelude
  using (_≡_; refl)
open import Cubical.Data.Bool.Base
  using (true)
open import Cubical.Data.List.Base
  using ([]; _∷_)

open import FF.Json
  using (JsonValue; jarray; jbool; jnumber; jstring; jnull)
-- Open the wrapper so the upstream `gen*` names emitted by the macro are also
-- in scope while Agda checks the generated term.
open import Spartan6.Unsafe.Json.Generate

generatedValue : JsonValue
generatedValue = jsonValueFromNode "[true,6,\"spartan\",null]"

generatedValue-reduces :
  generatedValue ≡
    jarray (jbool true ∷ jnumber 6 ∷ jstring "spartan" ∷ jnull ∷ [])
generatedValue-reduces = refl