ivor-0.1.11: Theorem proving library based on dependent type theory Source code Contents Index

Ivor.Primitives Portability non-portable Stability experimental Maintainer eb@dcs.st-and.ac.uk

Description

Some basic primitive types. Importing this module adds instances of ViewConst for Int, Float and String (Float is represented by Haskell Double). addPrimitives should be used to add these type constructors to the context.

Synopsis

addPrimitives :: Context -> TTM Context parsePrimitives :: Parser ViewTerm parsePrimTerm :: String -> TTM ViewTerm

Documentation

addPrimitives :: Context -> TTM Context Source

Add primitive types for Int, Float and String, and some primitive operations [add,sub,mult,div][int,float] and concat.

parsePrimitives :: Parser ViewTerm Source

Parse a primitive constant

parsePrimTerm :: String -> TTM ViewTerm Source

Parse a term including primitives

Produced by Haddock version 2.6.0