less prototype, less bad code implementation of CCHM type theory
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.
 
 
 

19 lines
325 B

module Presyntax.Presyntax where
import Data.Text (Text)
data Plicity
= Im | Ex
deriving (Eq, Show, Ord)
data Expr
= Var Text
| App Plicity Expr Expr
| Lam Plicity Text Expr
| Pi Plicity Text Expr Expr
deriving (Eq, Show, Ord)
data Statement
= Decl Text Expr
| Defn Text Expr
deriving (Eq, Show, Ord)