Notation.Hints

Definitions

0 NotationHint : Algebra sig -> (Type -> Type) -> Type

Visibility: public export

.notationHint : (0 a : Algebra sig) -> (0 notation : (Type -> Type)) -> notation (U a) -> NotationHint a notation

Visibility: public export

0 NotationHint : Model pres -> (Type -> Type) -> Type

Visibility: public export

.notationHint : (0 a : Model pres) -> (0 notation : (Type -> Type)) -> notation (U a) -> NotationHint a notation

Visibility: public export