Idris2Doc : Core.Unify

Core.Unify

(source)
Reexports
import public Core.UnifyState
Definitions
data UnifyMode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
InLHS : UnifyMode
  
InTerm : UnifyMode
  
InMatch : UnifyMode
  
InSearch : UnifyMode

  Hints:
  
Eq UnifyMode
  
Show UnifyMode
record UnifyInfo : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkUnifyInfo : Bool -> UnifyMode -> UnifyInfo

  Projections:
  
.atTop : UnifyInfo -> Bool
  
.umode : UnifyInfo -> UnifyMode

  Hint: 
Eq UnifyInfo
.atTop : UnifyInfo -> Bool
  Visibility: public export
atTop : UnifyInfo -> Bool
  Visibility: public export
.umode : UnifyInfo -> UnifyMode
  Visibility: public export
umode : UnifyInfo -> UnifyMode
  Visibility: public export
inTerm : UnifyInfo
  Visibility: export
inLHS : UnifyInfo
  Visibility: export
inMatch : UnifyInfo
  Visibility: export
inSearch : UnifyInfo
  Visibility: export
data AddLazy : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NoLazy : AddLazy
  
AddForce : LazyReason -> AddLazy
  
AddDelay : LazyReason -> AddLazy

  Hint: 
Show AddLazy
record UnifyResult : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkUnifyResult : List Int -> Bool -> List Int -> AddLazy -> UnifyResult

  Projections:
  
.addLazy : UnifyResult -> AddLazy
  
.constraints : UnifyResult -> List Int
  
.holesSolved : UnifyResult -> Bool
  
.namesSolved : UnifyResult -> List Int
.constraints : UnifyResult -> List Int
  Visibility: public export
constraints : UnifyResult -> List Int
  Visibility: public export
.holesSolved : UnifyResult -> Bool
  Visibility: public export
holesSolved : UnifyResult -> Bool
  Visibility: public export
.namesSolved : UnifyResult -> List Int
  Visibility: public export
namesSolved : UnifyResult -> List Int
  Visibility: public export
.addLazy : UnifyResult -> AddLazy
  Visibility: public export
addLazy : UnifyResult -> AddLazy
  Visibility: public export
interface Unify : (List Name -> Type) -> Type
  Parameters: tm
Methods:
  
unifyD : Ref Ctxt Defs -> Ref UST UState -> UnifyInfo -> FC -> Env Term vars -> tm vars -> tm vars -> Core UnifyResult
  
unifyWithLazyD : Ref Ctxt Defs -> Ref UST UState -> UnifyInfo -> FC -> Env Term vars -> tm vars -> tm vars -> Core UnifyResult

Implementations:
  
Unify NF
  
Unify Term
  
Unify Closure
unifyD : Unify tm => Ref Ctxt Defs -> Ref UST UState -> UnifyInfo -> FC -> Env Term vars -> tm vars -> tm vars -> Core UnifyResult
  Visibility: public export
unifyWithLazyD : Unify tm => Ref Ctxt Defs -> Ref UST UState -> UnifyInfo -> FC -> Env Term vars -> tm vars -> tm vars -> Core UnifyResult
  Visibility: public export
unify : Unify tm => Ref Ctxt Defs => Ref UST UState => UnifyInfo -> FC -> Env Term vars -> tm vars -> tm vars -> Core UnifyResult
  Visibility: export
unifyWithLazy : Unify tm => Ref Ctxt Defs => Ref UST UState => UnifyInfo -> FC -> Env Term vars -> tm vars -> tm vars -> Core UnifyResult
  Visibility: export
search : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Bool -> Nat -> Name -> Term vars -> Env Term vars -> Core (Term vars)
  Visibility: export
patternEnvTm : Ref Ctxt Defs => Ref UST UState => Env Term vars -> List (Term vars) -> Core (Maybe (newvars : List Name ** (List (Var newvars), Thin newvars vars)))
  Visibility: export
updateSolution : Ref Ctxt Defs => Ref UST UState => Env Term vars -> Term vars -> Term vars -> Core Bool
  Visibility: export
solveIfUndefined : Ref Ctxt Defs => Ref UST UState => Env Term vars -> Term vars -> Term vars -> Core Bool
  Visibility: export
unifyNoEta : Ref Ctxt Defs => Ref UST UState => UnifyInfo -> FC -> Env Term vars -> NF vars -> NF vars -> Core UnifyResult
  Visibility: export
setInvertible : Ref Ctxt Defs => FC -> Name -> Core ()
  Visibility: export
data SolveMode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Normal : SolveMode
  
Defaults : SolveMode
  
MatchArgs : SolveMode
  
LastChance : SolveMode

  Hint: 
Eq SolveMode
solveConstraints : Ref Ctxt Defs => Ref UST UState => UnifyInfo -> SolveMode -> Core ()
  Visibility: export
solveConstraintsAfter : Ref Ctxt Defs => Ref UST UState => Int -> UnifyInfo -> SolveMode -> Core ()
  Visibility: export
giveUpConstraints : Ref Ctxt Defs => Ref UST UState => Core ()
  Visibility: export
checkArgsSame : Ref UST UState => Ref Ctxt Defs => List Int -> Core Bool
  Visibility: export
checkDots : Ref UST UState => Ref Ctxt Defs => Core ()
  Visibility: export