Idris-dev/test/ffi005/Postulate.idr

module Main

%language TypeProviders

bad : IO (Provider Type)
bad = return $ pure Void

%provide postulate oops with bad

main : IO ()
main = putStrLn "oops"
Control whether provider decls accept postulates Extends the provider syntax to accept an optional "what" parameter, which controls if it can be satisfied with just proof terms, just postulates, or either. 2014-02-26 17:22:08 +04:00			`module Main`
Postulate providers Now, type providers don't need to return a proof - they can postulate new axioms. The intention is to connect this both to QuickCheck and to external proof oracles, such as SMT solvers. 2014-02-26 14:37:21 +04:00
			`%language TypeProviders`

Distinguish postulate providers and type providers at use site This is not backwards compatible, but as far as I know, there are no users of postulate providers who are not me. The old system allowed both the definition of the provider and the use site to be involved in the determination of what is a postulate and what is not. This is not good - users should always be in full control of this. The new implementation has two syntaxes: %provide (x : t) with p %provide postulate x with p The first is the type provider syntax we know and love. The second requires that the provider in fact return a type, which is then made into the type of the resulting postulate. 2014-06-05 15:49:24 +04:00			`bad : IO (Provider Type)`
Removed '_\|_' as a built in declaration and renamed it to 'Void', 'FalseElim' now 'VoidElim' to match up 2014-10-11 22:00:19 +04:00			`bad = return $ pure Void`
Postulate providers Now, type providers don't need to return a proof - they can postulate new axioms. The intention is to connect this both to QuickCheck and to external proof oracles, such as SMT solvers. 2014-02-26 14:37:21 +04:00
Distinguish postulate providers and type providers at use site This is not backwards compatible, but as far as I know, there are no users of postulate providers who are not me. The old system allowed both the definition of the provider and the use site to be involved in the determination of what is a postulate and what is not. This is not good - users should always be in full control of this. The new implementation has two syntaxes: %provide (x : t) with p %provide postulate x with p The first is the type provider syntax we know and love. The second requires that the provider in fact return a type, which is then made into the type of the resulting postulate. 2014-06-05 15:49:24 +04:00			`%provide postulate oops with bad`
Postulate providers Now, type providers don't need to return a proof - they can postulate new axioms. The intention is to connect this both to QuickCheck and to external proof oracles, such as SMT solvers. 2014-02-26 14:37:21 +04:00
Control whether provider decls accept postulates Extends the provider syntax to accept an optional "what" parameter, which controls if it can be satisfied with just proof terms, just postulates, or either. 2014-02-26 17:22:08 +04:00			`main : IO ()`
			`main = putStrLn "oops"`
Postulate providers Now, type providers don't need to return a proof - they can postulate new axioms. The intention is to connect this both to QuickCheck and to external proof oracles, such as SMT solvers. 2014-02-26 14:37:21 +04:00