module Generic.Unsafe.PrimAtom.Example where

open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.Macro
open import Generic.PrimAtom
open import Generic.Unsafe.PrimAtom.Macro

data StringChoice : Type₀ where
  string-empty : StringChoice
  text         : String → StringChoice
  pair         : String → String → StringChoice

genericStringChoice : Generic PrimAtoms StringChoice
genericStringChoice = deriveGenericIn PrimAtoms StringChoice

-- This launches the local Node.js UI during typechecking, so it is kept as an
-- opt-in example rather than a checked declaration:
--
-- chosenStringChoice : StringChoice
-- chosenStringChoice = choosePrimAtomValue genericStringChoice