See the official user manual for the most up-to-date version of the information on this page.
With postulates we can introduce elements in a type without actually giving the definition of the element itself.
The general form of a postulate declaration is as follow
postulate c11 ... c1i : <Type> ... cn1 ... cnj : <Type>
Example
postulate A B : Set a : A b : B _=AB=_ : A -> B -> Set a==b : a =AB= b
Introducing postulates is in general not something we recommend. Once postulates are introduced the consistency of the whole development is at risk, because there is nothing that prevents us from introducing an element in the empty set.
data False : Set where postulate bottom : False
A preferable way to work is to define a module parametrised by the elements we need
module Absurd (bt : False) where ... module M (A B : Set; a : A; b : B) (_=AB=_ : A -> B -> Set) (a==b : a =AB= b) where ...
Page last modified on December 14, 2018, at 03:56 pm
Powered by
PmWiki