idris-1.3.1: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
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

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

data FailContext Source #

Constructors

FailContext 
Instances
Eq FailContext Source # 
Instance details

Defined in Idris.Core.Unify

Show FailContext Source # 
Instance details

Defined in Idris.Core.Unify

data FailAt Source #

Constructors

Match 
Unify 
Instances
Eq FailAt Source # 
Instance details

Defined in Idris.Core.Unify

Methods

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

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

Show FailAt Source # 
Instance details

Defined in Idris.Core.Unify