wilbowma

#lang racket

;; A well typed macro that manipulates binding (in a trivial way)
(module A racket
  (require
   (for-syntax
    racket/function
    syntax/parse
    racket/syntax
    syntax/transformer))

wilbowma

{-# OPTIONS --guarded #-}


open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
open import Data.Unit using (⊤; tt)
open import Data.Nat -- using (ℕ; _+_; suc; _<_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; fromℕ<)
open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)

wilbowma

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical

cong : ∀ {ℓ} {A : Set ℓ} {x y : A} {B : A → Set ℓ} (f : (a : A) → B a) (p : x ≡ y)
       → PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)

open import Data.Nat

wilbowma

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ; _+_; suc)
open import Data.Nat.Properties using (+-cancel-≡; +-comm; +-assoc; _<?_; +-suc)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin hiding (suc; strengthen; _<?_) renaming (_+_ to _Fin+_)
open import Data.Vec

wilbowma

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ; _+_; suc)
open import Data.Nat.Properties using (+-cancel-≡; +-comm; +-assoc; _<?_; +-suc)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin hiding (suc; strengthen; _<?_) renaming (_+_ to _Fin+_)
open import Data.Vec

wilbowma

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ; _+_; suc)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin hiding (suc; strengthen) renaming (_+_ to _Fin+_)
open import Data.Vec

wilbowma

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin
open import Data.Vec

wilbowma

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product

-- A notion of model of STLC
-- A Theory for STLC

wilbowma

open import Data.Nat
open import Data.Bool hiding (_<_)
open import Data.List
open import Data.Fin hiding (_<_; _+_)
open import Data.Unit
open import Relation.Nullary
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- What is a semantics? A semantics defines the meaning of terms.

wilbowma

#lang racket/base

(require
 (for-syntax
  racket
  syntax/parse)
 racket/contracts)

(provide (rename-out [new-define/contract define/contract]))