Idris2Doc : Language.Reflection.VarSubst

Language.Reflection.VarSubst

(source)
Definitions
NameSet : Type
  SortedSet of Names

  Totality: total
  Visibility: public export
containsVariable : Name -> TTImp -> Bool
  Check if a TTImp contains a variable

  Totality: total
  Visibility: export
usesVariables : TTImp -> NameSet
  Calculate a set of used variables

  Totality: total
  Visibility: export
substituteVariables : SortedMap Name TTImp -> TTImp -> TTImp
  Substitute all occurrences of each variable with the given expression

  Totality: total
  Visibility: export
substituteVariable : Name -> TTImp -> TTImp -> TTImp
  Substitute all occurrences of given variable with given expression

  Totality: total
  Visibility: export
substituteBind : SortedMap Name TTImp -> TTImp -> TTImp
  Substitute all variable and BindVar occurrences with given

  Totality: total
  Visibility: export