Abt.Concrete.LocallyNameless

Documentation

data Tm o n where

Locally nameless terms with operators in o at arity n.

Constructors

Free :: Var -> Tm o Z

Bound :: Int -> Tm o Z

Abs :: Tm o n -> Tm o (S n)

App :: o ns -> HList (Tm o) ns -> Tm o Z

Instances

Show1 [Nat] o => Abt Var o (Tm o)

HEq1 [Nat] o => HEq1 Nat (Tm o)

data Var

A variable is a De Bruijn index, optionally decorated with a display name.

Constructors

Var

Fields

_varName :: !(Maybe String)

_varIndex :: !Int

Instances

Eq Var

Ord Var

Show Var

MonadVar Var M

Check out the source to see fresh variable generation.

Show1 [Nat] o => Abt Var o (Tm o)

varName :: Functor f => (Maybe String -> f (Maybe String)) -> Var -> f Var

A lens for _varName.

varName ∷ Lens' Var (Maybe String)

varIndex :: Functor f => (Int -> f Int) -> Var -> f Var

A lens for _varIndex.

varIndex ∷ Lens' Var Int