phile314

-- thrift source
namespace hs Thrift

# Trivial exception for testing only.
exception Exception {

  # The exception simply contains a message string.
  1: required string message;
}

phile314

module ReflApp where

open import Reflection
open import IO
open import Data.Unit
open import Data.List
import IO.Primitive

g : Term
g = app (lam visible (abs "x" (var 0 []))) [ (arg (arg-info visible relevant) (def (quote putStrLn) [ (arg (arg-info visible relevant) (quoteTerm "dfgdfg")) ])) ]

phile314

open import PiWare.Atom.Bool using (Atomic-B)
open import PiWare.Gates Atomic-B

module Test.RunWithIO (Gt : Gates) where
-- A = type of atoms

open import Data.Vec as Vec using (Vec)
open import Data.Nat as Nat using (ℕ; _≤?_; suc; _+_)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.String as String using (String; fromList; toList; Costring)