ocharles

{-# language ConstraintKinds #-}
{-# language FlexibleContexts #-}
{-# language FlexibleInstances #-}
{-# language GADTs #-}
{-# language MultiParamTypeClasses #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language RankNTypes #-}
{-# language QuantifiedConstraints #-}
{-# language TypeApplications #-}
{-# language TypeOperators #-}

ChristopherKing42

--Roughly based on https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs by Gabriel Gonzalez et al.

data Expr = Star | Box | Var Int | Lam Int Expr Expr | Pi Int Expr Expr | App Expr Expr deriving (Show, Eq)

subst v e (Var v')       | v == v' = e
subst v e (Lam v' ta b ) | v == v' = Lam v' (subst v e ta)            b
subst v e (Lam v' ta b )           = Lam v' (subst v e ta) (subst v e b )
subst v e (Pi  v' ta tb) | v == v' = Pi  v' (subst v e ta)            tb
subst v e (Pi  v' ta tb)           = Pi  v' (subst v e ta) (subst v e tb)
subst v e (App f a     )           = App    (subst v e f ) (subst v e a )

andrejbauer

(* An initial attempt at universal algebra in Coq.
   Author: Andrej Bauer <Andrej.Bauer@andrej.com>

   If someone knows of a less painful way of doing this, please let me know.

   We would like to define the notion of an algebra with given operations satisfying given
   equations. For example, a group has of three operations (unit, multiplication, inverse)
   and five equations (associativity, unit left, unit right, inverse left, inverse right).
*)