idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Core.ProofTerm

Description

Implements a proof state, some primitive tactics for manipulating proofs, and some high level commands for introducing new theorems, evaluation/checking inside the proof system, etc.

Synopsis

Documentation

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.