a type theory with equality based on setoids
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
module Presyntax where
|
|
|
|
import Data.Text (Text)
|
|
import Syntax (Plicity)
|
|
|
|
data RawExpr
|
|
= Rvar Text
|
|
| Rapp Plicity RawExpr RawExpr
|
|
| Rlam Plicity Text RawExpr
|
|
| Rpi Plicity Text RawExpr RawExpr
|
|
| Rlet Text RawExpr RawExpr RawExpr
|
|
| Rtype
|
|
| Rhole
|
|
|
|
| Rtop | Runit
|
|
| Rbot
|
|
| Req RawExpr RawExpr
|
|
| Rrefl
|
|
| Rcoe
|
|
| Rcong
|
|
| Rsym
|
|
|
|
| Rsigma Text RawExpr RawExpr
|
|
| Rpair RawExpr RawExpr
|
|
| Rproj1 RawExpr
|
|
| Rproj2 RawExpr
|
|
|
|
| RSrcPos (Int, Int) (Int, Int) RawExpr
|
|
deriving (Eq, Show, Ord)
|