Language.Tagless

This module is based on the paper
Dependent Tagless Final
by Nicoals Biri

Definitions

(-#) : Type -> Type -> Type

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 0

BinaryOp : Type -> Type

Totality: total
Visibility: public export

Ctx : Type

Totality: total
Visibility: public export

Env : Ctx -> Type

Totality: total
Visibility: public export