idris-1.3.1: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Core.ProofState

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.

Documentation

data ProofState Source #

Constructors

PS 

Fields

Instances
Show ProofState Source # 
Instance details

Defined in Idris.Core.ProofState

newProof Source #

Arguments

:: Name

the name of what's to be elaborated

-> String

current source file

-> Context

the current global context

-> Ctxt TypeInfo

the value of the idris_datatypes field of IState

-> Int

the value of the idris_name field of IState

-> Type

the goal type

-> ProofState 

data Goal Source #

Constructors

GD 

dropGiven :: (Eq a, Foldable t1, Foldable t2) => t1 a -> [(a, TT a)] -> t2 a -> [(a, TT a)] Source #

keepGiven :: (Eq a, Foldable t1, Foldable t2) => t1 a -> [(a, TT a)] -> t2 a -> [(a, TT a)] Source #