16 lines
348 B
Agda
16 lines
348 B
Agda
|
open import Data.String
|
||
|
|
|
||
|
|
-- Chapter 3.6
|
||
|
|
data Arity : Set where
|
||
|
|
zero : Arity
|
||
|
|
_⊗_ : Arity → Arity → Arity
|
||
|
|
_-→_ : Arity → Arity → Arity
|
||
|
|
|
||
|
|
data Expr : Set where
|
||
|
|
Var : String → Arity → Expr
|
||
|
|
PrimConst : Arity → Expr
|
||
|
|
App : Expr → Expr → Expr
|
||
|
|
Abs : String → Expr → Expr
|
||
|
|
|
||
|
|
arity-of : (e : Expr) → Arity
|