idris-1.1.1: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
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

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

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