Language.Syntactic.Constructs.Identity

Identity function

Documentation

data Identity ctx a where

Identity function

Constructors

Id :: Sat ctx a => Identity ctx (a :-> Full a)

Instances

MaybeWitnessSat ctx1 (Identity ctx2)

MaybeWitnessSat ctx (Identity ctx)

WitnessSat (Identity ctx)

WitnessCons (Identity ctx)

ExprEq (Identity ctx)

ToTree (Identity ctx)

Render (Identity ctx)

Eval (Identity ctx)

Semantic (Identity ctx)

EvalBind (Identity ctx)

(:<: (Identity ctx') dom, Optimize dom ctx dom) => Optimize (Identity ctx') ctx dom

AlphaEq dom dom dom env => AlphaEq (Identity ctx) (Identity ctx) dom env