Idris2Doc : Language.Reflection.Expr

Language.Reflection.Expr

(source)
Reexports
import public Control.Applicative.Const
import public Data.Bits
import public Data.Cozippable
import public Data.Fin.Set
import public Data.Fin.ToFin
import public Data.List.Ex
import public Data.List.Quantifiers
import public Data.SortedSet
import public Data.These
import public Data.Vect.Dependent
import public Language.Reflection
import public Language.Reflection.Syntax
import public Syntax.IHateParens.List
Definitions
data IsNamedArg : Arg -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsNamed : IsNamedArg (MkArg cnt pii (Just n) ty)
isNamedArg : (arg : Arg) -> Dec (IsNamedArg arg)
  Totality: total
  Visibility: public export
stname : Maybe Name -> Name
  Totality: total
  Visibility: public export
argName : (a : Arg) -> {auto 0 _ : IsNamedArg a} -> Name
  Totality: total
  Visibility: public export
argName' : Arg -> Name
  Totality: total
  Visibility: public export
cleanupNamedHoles : TTImp -> TTImp
  Totality: total
  Visibility: export
cleanupArg : Arg -> Arg
  Run `cleanupNamedHoles` over all `Arg`'s `TTImp`s

  Totality: total
  Visibility: public export
argNames : (l : List Arg) -> {auto 0 _ : All IsNamedArg l} -> List Name
  Totality: total
  Visibility: export
normaliseAs' : Elaboration m => (0 expected : Type) -> (TTImp -> TTImp) -> {0 resulting : expected -> Type} -> (0 _ : ((x : expected) -> resulting x)) -> TTImp -> m TTImp
  Totality: total
  Visibility: export
normaliseAs : Elaboration m => (0 _ : Type) -> TTImp -> m TTImp
  Totality: total
  Visibility: public export
normalise : Elaboration m => TTImp -> m TTImp
  Totality: total
  Visibility: public export
normaliseAsType : Elaboration m => TTImp -> m TTImp
  Totality: total
  Visibility: public export
data AnyApp : Type
  Totality: total
  Visibility: public export
  Constructors:
  
PosApp : TTImp -> AnyApp
  
NamedApp : Name -> TTImp -> AnyApp
  
AutoApp : TTImp -> AnyApp
  
WithApp : TTImp -> AnyApp
appArg : Arg -> TTImp -> AnyApp
  Totality: total
  Visibility: public export
getExpr : AnyApp -> TTImp
  Totality: total
  Visibility: public export
mapExpr : (TTImp -> TTImp) -> AnyApp -> AnyApp
  Totality: total
  Visibility: public export
unAppAny : TTImp -> (TTImp, List AnyApp)
  Totality: total
  Visibility: public export
reAppAny1 : TTImp -> AnyApp -> TTImp
  Totality: total
  Visibility: public export
reAppAny : Foldable f => TTImp -> f AnyApp -> TTImp
  Totality: total
  Visibility: public export
liftList : Foldable f => f TTImp -> TTImp
  Lifts the given foldable of elements to an expression of a list-like data type

  Totality: total
  Visibility: public export
liftList' : Foldable f => f TTImp -> TTImp
  Lifts the given foldable of elements to an expression of `Prelude.List`

  Totality: total
  Visibility: public export
applySyn : TTImp -> TTImp -> TTImp
  Totality: total
  Visibility: public export
unDPair : TTImp -> (List Arg, TTImp)
  Totality: total
  Visibility: public export
unDPairUnAlt : TTImp -> Maybe (List Arg, TTImp)
  Totality: total
  Visibility: public export
buildDPair : TTImp -> List (Name, TTImp) -> TTImp
  Totality: total
  Visibility: public export
unNS : Name -> (List String, Name)
  Returns unnamespaced name and list of all namespaces stored in direct order
  
  Say, for `Data.Vect.Vect` it would return (["Data", "Vect"], `{Vect}).

  Totality: total
  Visibility: export
allNameSuffixes : Name -> List Name
  Returns all names that are suffixes of a given name (including the original name itself).
  
  For example, for the name `Data.Vect.Vect` suffixes set would include
  `Data.Vect.Vect`, `Vect.Vect` and `Vect`.

  Totality: total
  Visibility: export
isNamespaced : Name -> Bool
  Totality: total
  Visibility: export
isImplicit : PiInfo c -> Bool
  Totality: total
  Visibility: public export
isSameTypeAs : Name -> Name -> Elab Bool
  Totality: total
  Visibility: public export
nameConformsTo : Name -> Name -> Bool
  Totality: total
  Visibility: export
allVarNames' : TTImp -> SortedSet Name
  Totality: total
  Visibility: export
allVarNames : TTImp -> List Name
  Totality: total
  Visibility: export
isVar : TTImp -> Bool
  Totality: total
  Visibility: public export
0 ArgDeps : Nat -> Type
  Totality: total
  Visibility: public export
argDeps : (args : List Arg) -> ArgDeps (args .length)
  Totality: total
  Visibility: export
dependees : (args : List Arg) -> FinSet (args .length)
  Totality: total
  Visibility: export