Dan's 數位πŸͺ΄εœ’

Intrinsically typed term

1 min read

misc 
{-# OPTIONS --cubical #-}
module agda.intrinsical where
open import Agda.Primitive
open import Cubical.Foundations.Prelude
open import Cubical.Data.List

data Ty : Type where
  bool : Ty
  _β‡’_ : Ty β†’ Ty β†’ Ty

variable S T : Ty

Ctx = List Ty
_,,_ : Ctx β†’ Ty β†’ Ctx
Ξ“ ,, T = T ∷ Ξ“
infix 10 _,,_

variable Ξ“ : Ctx

Intrinsically-scoped de Brujin indices

data _βˆ‹_ : Ctx β†’ Ty β†’ Type where
  zero : Ξ“ ,, T βˆ‹ T
  suc : Ξ“ βˆ‹ T β†’ Ξ“ ,, S βˆ‹ T
infix 5 _βˆ‹_

variable x : Ξ“ βˆ‹ T

Intrinsically-typed terms

data _⊒_ : Ctx β†’ Ty β†’ Type where
  true false : Ξ“ ⊒ bool
  var : Ξ“ βˆ‹ T β†’ Ξ“ ⊒ T
  lam_ : Ξ“ ,, S ⊒ T β†’ Ξ“ ⊒ S β‡’ T
  _Β·_ : Ξ“ ⊒ S β‡’ T β†’ Ξ“ ⊒ S β†’ Ξ“ ⊒ T
  if_then_else_ : Ξ“ ⊒ bool β†’ Ξ“ ⊒ T β†’ Ξ“ ⊒ T β†’ Ξ“ ⊒ T
infix 9 _⊒_

Graph View

Backlinks