Skip to content

Instantly share code, notes, and snippets.

View wilbowma's full-sized avatar

William J. Bowman wilbowma

View GitHub Profile
#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))
{-# 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)
{-# 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
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
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
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
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
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
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.
#lang racket/base
(require
(for-syntax
racket
syntax/parse)
racket/contracts)
(provide (rename-out [new-define/contract define/contract]))