idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
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

Instances details
Show ProofState Source # 
Instance details

Defined in Idris.Core.ProofState

Methods

showsPrec :: Int -> ProofState -> ShowS

show :: ProofState -> String

showList :: [ProofState] -> ShowS

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 t, Foldable t) => t a -> [(a, TT a)] -> t a -> [(a, TT a)] Source #

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