Idris2Doc : Core.Name.Scoped

Core.Name.Scoped

(source)
Reexports
import public Core.Name
import public Libraries.Data.List.Thin
Definitions
Scopeable : Type -> Type
  Something which is having similar order as Scope itself

  Totality: total
  Visibility: public export
Scope : Type
  A scope is represented by a list of names. E.g. in the following
  rule, the scope Γ is extended with x when going under the λx.
  binder:
  
     Γ, x ⊢ t : B
   -----------------------------
     Γ    ⊢ λx. t : A → B

  Totality: total
  Visibility: public export
empty : Scopeable a
  Totality: total
  Visibility: public export
addInner : Scopeable a -> Scopeable a -> Scopeable a
  Totality: total
  Visibility: public export
bind : Scopeable a -> a -> Scopeable a
  Totality: total
  Visibility: public export
single : a -> Scopeable a
  Totality: total
  Visibility: public export
Scoped : Type
  A scoped definition is one indexed by a scope

  Totality: total
  Visibility: public export
scopeEq : (xs : Scope) -> (ys : Scope) -> Maybe (xs = ys)
  Totality: total
  Visibility: export
mkFresh : Scope -> Name -> Name
  Totality: total
  Visibility: export
data CompatibleVars : List a -> List a -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Pre : CompatibleVars xs xs
  
Ext : CompatibleVars xs ys -> CompatibleVars (n :: xs) (m :: ys)
invertExt : CompatibleVars (n :: xs) (m :: ys) -> CompatibleVars xs ys
  Totality: total
  Visibility: export
extendCompats : (args : List a) -> CompatibleVars xs ys -> CompatibleVars (args ++ xs) (args ++ ys)
  Totality: total
  Visibility: export
decCompatibleVars : (xs : List a) -> (ys : List a) -> Dec (CompatibleVars xs ys)
  Totality: total
  Visibility: export
areCompatibleVars : (xs : List a) -> (ys : List a) -> Maybe (CompatibleVars xs ys)
  Totality: total
  Visibility: export
0 Weakenable : Scoped -> Type
  Totality: total
  Visibility: public export
0 Strengthenable : Scoped -> Type
  Totality: total
  Visibility: public export
0 GenWeakenable : Scoped -> Type
  Totality: total
  Visibility: public export
0 Thinnable : Scoped -> Type
  Totality: total
  Visibility: public export
0 Shrinkable : Scoped -> Type
  Totality: total
  Visibility: public export
0 Embeddable : Scoped -> Type
  Totality: total
  Visibility: public export
interface Weaken : Scoped -> Type
  Parameters: tm
Constructor: 
MkWeaken

Methods:
  
weaken : tm vars -> tm (nm :: vars)
  
weakenNs : Weakenable tm

Implementations:
  
Weaken ArgType
  
Weaken (PatInfo p)
  
Weaken (NamedPats todo)
  
Weaken (IVars vs)
  
Weaken WkCExp
  
Weaken NestedNames
  
Weaken CaseTree
  
Weaken CExp
  
Weaken CConAlt
  
Weaken VarSet
  
Weaken Term
  
Weaken Var
  
Weaken (NVar nm)
weaken : Weaken tm => tm vars -> tm (nm :: vars)
  Totality: total
  Visibility: public export
weakenNs : Weaken tm => Weakenable tm
  Totality: total
  Visibility: public export
interface GenWeaken : Scoped -> Type
  Parameters: tm
Constructor: 
MkGenWeaken

Methods:
  
genWeakenNs : GenWeakenable tm

Implementations:
  
GenWeaken Term
  
GenWeaken Var
  
GenWeaken (NVar nm)
genWeakenNs : GenWeaken tm => GenWeakenable tm
  Totality: total
  Visibility: public export
genWeaken : GenWeaken tm => SizeOf local -> tm (local ++ outer) -> tm (local ++ (n :: outer))
  Totality: total
  Visibility: export
interface Strengthen : Scoped -> Type
  Parameters: tm
Constructor: 
MkStrengthen

Methods:
  
strengthenNs : Strengthenable tm

Implementations:
  
Strengthen Var
  
Strengthen (NVar nm)
strengthenNs : Strengthen tm => Strengthenable tm
  Totality: total
  Visibility: public export
strengthen : Strengthen tm => tm (nm :: vars) -> Maybe (tm vars)
  Totality: total
  Visibility: export
interface FreelyEmbeddable : Scoped -> Type
  Parameters: tm
Constructor: 
MkFreelyEmbeddable

Methods:
  
embed : Embeddable tm

Implementations:
  
FreelyEmbeddable CaseTree
  
FreelyEmbeddable CExp
  
FreelyEmbeddable VarSet
  
FreelyEmbeddable Term
  
FreelyEmbeddable (IsVar x k)
  
FreelyEmbeddable Var
  
FreelyEmbeddable (NVar nm)
embed : FreelyEmbeddable tm => Embeddable tm
  Totality: total
  Visibility: public export
FunctorFreelyEmbeddable : Functor f => FreelyEmbeddable tm => FreelyEmbeddable (f . tm)
  Totality: total
  Visibility: export
ListFreelyEmbeddable : FreelyEmbeddable tm => FreelyEmbeddable (List . tm)
  Totality: total
  Visibility: export
MaybeFreelyEmbeddable : FreelyEmbeddable tm => FreelyEmbeddable (Maybe . tm)
  Totality: total
  Visibility: export
GenWeakenWeakens : GenWeaken tm => Weaken tm
  Totality: total
  Visibility: export
FunctorGenWeaken : Functor f => GenWeaken tm => GenWeaken (f . tm)
  Totality: total
  Visibility: export
FunctorWeaken : Functor f => Weaken tm => Weaken (f . tm)
  Totality: total
  Visibility: export
ListWeaken : Weaken tm => Weaken (List . tm)
  Totality: total
  Visibility: export
MaybeWeaken : Weaken tm => Weaken (Maybe . tm)
  Totality: total
  Visibility: export
interface IsScoped : Scoped -> Type
  Parameters: tm
Constraints: Weaken tm
Methods:
  
compatNs : CompatibleVars xs ys -> tm xs -> tm ys
  
thin : Thinnable tm
  
shrink : Shrinkable tm

Implementations:
  
IsScoped Term
  
IsScoped Var
compatNs : IsScoped tm => CompatibleVars xs ys -> tm xs -> tm ys
  Totality: total
  Visibility: public export
thin : IsScoped tm => Thinnable tm
  Totality: total
  Visibility: public export
shrink : IsScoped tm => Shrinkable tm
  Totality: total
  Visibility: public export
compat : IsScoped tm => tm (m :: xs) -> tm (n :: xs)
  Totality: total
  Visibility: export