Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: 203a4359a7
Fetching contributors…

Cannot retrieve contributors at this time

82 lines (74 sloc) 4.505 kb
Name: ivor
Version: 0.1.10.1
Author: Edwin Brady
License: BSD3
License-file: LICENSE
Author: Edwin Brady
Maintainer: Edwin Brady <eb@dcs.st-and.ac.uk>
Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/
Stability: experimental
Build-depends: base, haskell98, parsec, mtl, directory, containers
Extensions: MultiParamTypeClasses, FunctionalDependencies,
ExistentialQuantification, OverlappingInstances
Category: Theorem provers, Dependent Types
Synopsis: Theorem proving library based on dependent type theory
Description: Ivor is a type theory based theorem prover, with a
Haskell API, designed for easy extending and embedding
of theorem proving technology in Haskell
applications. It provides an implementation of the
type theory and tactics for building terms, more or
less along the lines of systems such as Coq or Agda,
and taking much of its inspiration from Conor
McBride's presentation of OLEG.
.
The API provides a collection of primitive tactics and
combinators for building new tactics. It is therefore
possible to build new tactics to suit specific
applications. Ivor features a dependent type theory
similar to Luo's ECC with definitions (and similar to
that implemented in Epigram), with dependent pattern
matching, and experimental multi-stage programming
support. Optionally, it can be extended with
heterogeneous equality, primitive types and operations,
new parser rules, user defined tactics and (if you
want your proofs to be untrustworthy) a fixpoint
combinator.
Data-files: BUGS, INSTALL, TODO, docs/macros.ltx, docs/local.ltx, docs/tt.tex, docs/conclusion.tex,
docs/intro.tex, docs/hcar.sty, docs/tactics.tex, docs/library.ltx,
docs/shell.tex, docs/dtp.bib, docs/HCAR.tex, docs/Makefile,
docs/combinators.tex, docs/humett.tex, docs/interface.tex,
papers/tutorial/tutorial.tex, papers/tutorial/macros.ltx, papers/tutorial/theoremproving.tex,
papers/tutorial/introduction.tex, papers/tutorial/hslibrary.tex, papers/tutorial/library.ltx,
papers/tutorial/programming.tex, papers/tutorial/Makefile, papers/bib/literature.bib,
papers/ivor/examples.tex, papers/ivor/code.tex, papers/ivor/macros.ltx,
papers/ivor/ivor.tex, papers/ivor/corett.tex, papers/ivor/conclusions.tex,
papers/ivor/intro.tex, papers/ivor/llncs.cls, papers/ivor/tactics.tex,
papers/ivor/library.ltx, papers/ivor/dtp.bib, papers/ivor/alink.bib,
papers/ivor/Makefile, papers/ivor/embounded.bib
Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, examplett/partial.tt, examplett/nat.tt,
examplett/vec.tt, examplett/lt.tt, examplett/Test.hs, examplett/plus.tt,
examplett/jmeq.tt, examplett/eq.tt, examplett/logic.tt, examplett/interp.tt,
examplett/stageplus.tt, examplett/Nat.hs, examplett/general.tt, examplett/natsimpl.tt,
examplett/test.tt, examplett/vect.tt, examplett/fin.tt, examplett/ack.tt,
IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs,
lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,
lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt
Build-depends: base >=3 && <5, parsec, mtl, directory, binary
Build-type: Simple
Extensions: MultiParamTypeClasses, FunctionalDependencies,
ExistentialQuantification, OverlappingInstances,
TypeSynonymInstances, PatternGuards
-- Needs some -Wall cleanup
-- GHC-options: -Wall
Exposed-modules:
Ivor.TT, Ivor.Shell, Ivor.Primitives,
Ivor.TermParser, Ivor.ViewTerm, Ivor.Equality,
Ivor.Plugin, Ivor.Construction
Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State,
Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator
Ivor.Gadgets, Ivor.SC, Ivor.Bytecode, Ivor.Values,
Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,
Ivor.RunTT, Ivor.Compiler, Ivor.Prefix, Ivor.Errors,
Ivor.PatternDefs, Ivor.ShellState, Ivor.Scopecheck
Jump to Line
Something went wrong with that request. Please try again.