blob: 3545f9a5e36a43bbbe2882026a86affeadd06d45 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# OPTIONS --without-K --safe #-}
module Cfe.Expression.Base
{ℓ} (A : Set ℓ)
where
open import Data.Nat
data Expression : ℕ → Set ℓ where
⊥ : {n : ℕ} → Expression n
ε : {n : ℕ} → Expression n
Char : {n : ℕ} → A → Expression n
_∨_ : {n : ℕ} → Expression n → Expression n → Expression n
_∙_ : {n : ℕ} → Expression n → Expression n → Expression n
Var : {m : ℕ} → (n : ℕ) → Expression (suc (m + n))
μ : {n : ℕ} → Expression (suc n) → Expression n
|
