Expr.agda
1module Expr where
2
3open import Variable
4
5
6data BinaryOp : Set where
7 -- Arithmetical
8 plus minus mult div power : BinaryOp
9 -- Logical operations
10 equal and or : BinaryOp
11
12data UnaryOp : Set where
13 not : UnaryOp
14
15data Expr : Set where
16 var : Variable → Expr
17 binary : BinaryOp → Expr → Expr → Expr
18 unary : UnaryOp → Expr → Expr
19 constant : Value → Expr