Core.Name.CompatibleVars

Definitions

data CompatibleVars : SnocList a -> SnocList a -> Type

Totality: total
Visibility: public export
Constructors:

Pre : CompatibleVars xs xs

Ext : CompatibleVars xs ys -> CompatibleVars (xs :< n) (ys :< m)

invertExt : CompatibleVars (xs :< n) (ys :< m) -> CompatibleVars xs ys

Visibility: export

extendCompats : (args : SnocList a) -> CompatibleVars xs ys -> CompatibleVars (xs ++ args) (ys ++ args)

Visibility: export

decCompatibleVars : (xs : SnocList a) -> (ys : SnocList a) -> Dec (CompatibleVars xs ys)

Visibility: export

areCompatibleVars : (xs : SnocList a) -> (ys : SnocList a) -> Maybe (CompatibleVars xs ys)

Visibility: export