This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- thrift source | |
namespace hs Thrift | |
# Trivial exception for testing only. | |
exception Exception { | |
# The exception simply contains a message string. | |
1: required string message; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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")) ])) ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |