idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Core.Unify

Description

Unification is applied inside the theorem prover. We're looking for holes which can be filled in, by matching one term's normal form against another. Returns a list of hole names paired with the term which solves them, and a list of things which need to be injective.

Documentation

match_unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] -> TC [(Name, TT Name)] Source #

unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [Name] -> [FailContext] -> TC ([(Name, TT Name)], Fails) Source #

type Fails = [(TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)] Source #

data FailContext Source #

Constructors

FailContext 

Instances

Instances details
Show FailContext Source # 
Instance details

Defined in Idris.Core.Unify

Methods

showsPrec :: Int -> FailContext -> ShowS

show :: FailContext -> String

showList :: [FailContext] -> ShowS

Eq FailContext Source # 
Instance details

Defined in Idris.Core.Unify

Methods

(==) :: FailContext -> FailContext -> Bool

(/=) :: FailContext -> FailContext -> Bool

data FailAt Source #

Constructors

Match 
Unify 

Instances

Instances details
Show FailAt Source # 
Instance details

Defined in Idris.Core.Unify

Methods

showsPrec :: Int -> FailAt -> ShowS

show :: FailAt -> String

showList :: [FailAt] -> ShowS

Eq FailAt Source # 
Instance details

Defined in Idris.Core.Unify

Methods

(==) :: FailAt -> FailAt -> Bool

(/=) :: FailAt -> FailAt -> Bool