Idris.Syntax.Views

Definitions

data Arg' : Type -> Type

Totality: total
Visibility: public export
Constructors:

Explicit : FC -> PTerm' nm -> Arg' nm

Auto : FC -> PTerm' nm -> Arg' nm

Named : FC -> Name -> PTerm' nm -> Arg' nm

unArg : Arg' nm -> PTerm' nm

Totality: total
Visibility: export

getFnArgs : (Name -> nm) -> PTerm' nm -> (PTerm' nm, List (Arg' nm))

Totality: total
Visibility: export

underPis : PTerm' nm -> (List (Maybe Name, Binder (PTerm' nm)), PTerm' nm)

Totality: total
Visibility: export

underLams : PTerm' nm -> (List (PTerm' nm, Binder (PTerm' nm)), PTerm' nm)

Totality: total
Visibility: export