idris-1.3.1: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Core.ProofTerm

Description

 
Synopsis

Documentation

data ProofTerm Source #

Instances
Show ProofTerm Source # 
Instance details

Defined in Idris.Core.ProofTerm

data Goal Source #

Constructors

GD 

updateSolvedTerm :: [(Name, Term)] -> Term -> Term Source #

Given a list of solved holes, fill out the solutions in a term

updateSolvedTerm' :: [(Name, Term)] -> Term -> (Term, Bool) Source #

Given a list of solved holes, fill out the solutions in a term. Return whether updates were performed, to facilitate sharing when there are no updates.

refocus :: Hole -> ProofTerm -> ProofTerm Source #

Refocus the proof term zipper on a particular hole, if it exists. If not, return the original proof term.

updsubst Source #

Arguments

:: Eq n 
=> n

The id to replace

-> TT n

The replacement term

-> TT n

The term to replace in

-> TT n 

As subst, in TT, but takes advantage of knowing not to substitute under Complete applications.