Idris2Doc : Core.TT.Var

Core.TT.Var

(source)
Definitions
data IsVar : a -> Nat -> List a -> Type
  IsVar n k ns is a proof that
  the name n
  is a position k
  in the snoclist ns

  Totality: total
  Visibility: public export
  Constructors:
  
First : IsVar n 0 (n :: ns)
  
Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

  Hint: 
FreelyEmbeddable (IsVar x k)
0 Last : HasLength (S n) vs -> Exists (\nm => IsVar nm n vs)
  Totality: total
  Visibility: export
finIdx : (0 _ : IsVar x idx vars) -> Fin (length vars)
  Totality: total
  Visibility: export
nameAt : (0 _ : IsVar n idx vars) -> a
  Recover the value pointed at by an IsVar proof
  O(n) in the size of the index

  Totality: total
  Visibility: export
dropLater : IsVar nm (S idx) (n :: ns) -> IsVar nm idx ns
  Inversion principle for Later

  Totality: total
  Visibility: export
0 mkIsVar : HasLength m inner -> IsVar nm m (inner ++ (nm :: outer))
  Totality: total
  Visibility: export
0 mkIsVarChiply : HasLength m inner -> IsVar nm m (inner <>> (nm :: outer))
  Totality: total
  Visibility: export
dropIsVar : (ns : List a) -> (0 _ : IsVar name idx ns) -> List a
  Compute the remaining scope once the target variable has been removed

  Totality: total
  Visibility: public export
0 embedIsVar : IsVar x idx xs -> IsVar x idx (xs ++ outer)
  Throw in extra variables on the outer side of the context
  This is essentially the identity function
  This is slow so we ensure it's only used in a runtime irrelevant manner

  Totality: total
  Visibility: export
0 weakenIsVar : (s : SizeOf ns) -> IsVar x idx xs -> IsVar x (size s + idx) (ns ++ xs)
  Throw in extra variables on the local end of the context.
  This is slow so we ensure it's only used in a runtime irrelevant manner

  Totality: total
  Visibility: export
locateIsVar : (s : SizeOf local) -> (0 _ : IsVar x idx (local ++ outer)) -> Either (Erased (IsVar x idx local)) (Erased (IsVar x (minus idx (size s)) outer))
  Totality: total
  Visibility: export
record Var : List a -> Type
  A variable in a scope is a name, a De Bruijn index,
  and a proof that the name is at that position in the scope.
  Everything but the De Bruijn index is erased.

  Totality: total
  Visibility: public export
  Constructor: 
MkVar : (0 _ : IsVar varNm varIdx vars) -> Var vars

  Projections:
  
.varIdx : Var vars -> Nat
  
0 .varNm : Var vars -> a
  
0 .varPrf : ({rec:0} : Var vars) -> IsVar (varNm {rec:0}) (varIdx {rec:0}) vars

  Hints:
  
Eq (Var xs)
  
FreelyEmbeddable Var
  
GenWeaken Var
  
Hashable (Var vars)
  
IsScoped Var
  
Show (Var ns)
  
Strengthen Var
  
Weaken Var
.varIdx : Var vars -> Nat
  Totality: total
  Visibility: public export
varIdx : Var vars -> Nat
  Totality: total
  Visibility: public export
0 .varNm : Var vars -> a
  Totality: total
  Visibility: public export
0 varNm : Var vars -> a
  Totality: total
  Visibility: public export
0 .varPrf : ({rec:0} : Var vars) -> IsVar (varNm {rec:0}) (varIdx {rec:0}) vars
  Totality: total
  Visibility: public export
0 varPrf : ({rec:0} : Var vars) -> IsVar (varNm {rec:0}) (varIdx {rec:0}) vars
  Totality: total
  Visibility: public export
first : Var (n :: ns)
  Totality: total
  Visibility: export
later : Var ns -> Var (n :: ns)
  Totality: total
  Visibility: export
isLater : Var (n :: vs) -> Maybe (Var vs)
  Totality: total
  Visibility: export
last : SizeOf vs -> Maybe (Var vs)
  Totality: total
  Visibility: export
mkVar : SizeOf inner -> Var (inner ++ (nm :: outer))
  Totality: total
  Visibility: export
mkVarChiply : SizeOf inner -> Var (inner <>> (nm :: outer))
  Totality: total
  Visibility: export
allVars : (vars : Scope) -> List (Var vars)
  Generate all variables

  Totality: total
  Visibility: export
record NVar : a -> List a -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkNVar : (0 _ : IsVar nm nvarIdx vars) -> NVar nm vars

  Projections:
  
.nvarIdx : NVar nm vars -> Nat
  
0 .nvarPrf : ({rec:0} : NVar nm vars) -> IsVar nm (nvarIdx {rec:0}) vars

  Hints:
  
FreelyEmbeddable (NVar nm)
  
GenWeaken (NVar nm)
  
Strengthen (NVar nm)
  
Weaken (NVar nm)
.nvarIdx : NVar nm vars -> Nat
  Totality: total
  Visibility: public export
nvarIdx : NVar nm vars -> Nat
  Totality: total
  Visibility: public export
0 .nvarPrf : ({rec:0} : NVar nm vars) -> IsVar nm (nvarIdx {rec:0}) vars
  Totality: total
  Visibility: public export
0 nvarPrf : ({rec:0} : NVar nm vars) -> IsVar nm (nvarIdx {rec:0}) vars
  Totality: total
  Visibility: public export
first : NVar n (n :: ns)
  Totality: total
  Visibility: export
later : NVar nm ns -> NVar nm (n :: ns)
  Totality: total
  Visibility: export
isLater : NVar nm (n :: ns) -> Maybe (NVar nm ns)
  Totality: total
  Visibility: export
forgetName : NVar nm vars -> Var vars
  Totality: total
  Visibility: export
recoverName : (v : Var vars) -> NVar (varNm v) vars
  Totality: total
  Visibility: export
mkNVar : SizeOf inner -> NVar nm (inner ++ (nm :: outer))
  Totality: total
  Visibility: export
mkNVarChiply : SizeOf inner -> NVar nm (inner <>> (nm :: outer))
  Totality: total
  Visibility: export
locateNVar : SizeOf local -> NVar nm (local ++ outer) -> Either (NVar nm local) (NVar nm outer)
  Totality: total
  Visibility: export
dropNVar : NVar nm ns -> List a
  Totality: total
  Visibility: public export
isDeBruijn : Nat -> (vars : List Name) -> Maybe (Var vars)
  Totality: total
  Visibility: export
isNVar : (n : Name) -> (ns : List Name) -> Maybe (NVar n ns)
  Totality: total
  Visibility: export
isVar : Name -> (ns : List Name) -> Maybe (Var ns)
  Totality: total
  Visibility: export
locateVar : SizeOf local -> Var (local ++ outer) -> Either (Var local) (Var outer)
  Totality: total
  Visibility: export
weakenNVar : SizeOf ns -> NVar name outer -> NVar name (ns ++ outer)
  Totality: total
  Visibility: export
embedNVar : NVar name ns -> NVar name (ns ++ outer)
  Totality: total
  Visibility: export
insertNVar : SizeOf local -> NVar nm (local ++ outer) -> NVar nm (local ++ (n :: outer))
  Totality: total
  Visibility: export
insertNVarChiply : SizeOf local -> NVar nm (local <>> outer) -> NVar nm (local <>> (n :: outer))
  Totality: total
  Visibility: export
insertNVarNames : GenWeakenable (NVar name)
  Totality: total
  Visibility: export
removeNVar : SizeOf local -> NVar nm (local ++ (n :: outer)) -> Maybe (NVar nm (local ++ outer))
  The (partial) inverse to insertNVar

  Totality: total
  Visibility: export
insertVar : SizeOf local -> Var (local ++ outer) -> Var (local ++ (n :: outer))
  Totality: total
  Visibility: export
removeVar : SizeOf local -> Var (local ++ (n :: outer)) -> Maybe (Var (local ++ outer))
  The (partial) inverse to insertVar

  Totality: total
  Visibility: export
strengthenIsVar : (s : SizeOf inner) -> (0 _ : IsVar x n (inner ++ vars)) -> Maybe (Erased (IsVar x (minus n (size s)) vars))
  Totality: total
  Visibility: export
thinIsVar : (0 _ : IsVar name idx xs) -> Thin xs ys -> Var ys
  Totality: total
  Visibility: export
shrinkIsVar : (0 _ : IsVar name idx xs) -> Thin ys xs -> Maybe (Var ys)
  Totality: total
  Visibility: export
0 FreelyEmbeddableIsVar : FreelyEmbeddable (IsVar x k)
  Totality: total
  Visibility: export
WeakenVar : Weaken Var
  Totality: total
  Visibility: export
WeakenNVar : Weaken (NVar nm)
  Totality: total
  Visibility: export
shiftUnderNs : SizeOf inner -> (0 _ : IsVar n idx (x :: (inner ++ outer))) -> NVar n (inner ++ (x :: outer))
  Moving the zeroth variable under a set number of variables

  Totality: total
  Visibility: export