Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 85 lines (76 sloc) 4.547 kB
4a53940 Initial version
eb authored
1 Name: ivor
613fef1 Some helpers for Idris
eb authored
2 Version: 0.1.13
4a53940 Initial version
eb authored
3 Author: Edwin Brady
4 License: BSD3
5 License-file: LICENSE
491515a @gwern rearrange cabal fields
gwern authored
6 Author: Edwin Brady
7 Maintainer: Edwin Brady <eb@dcs.st-and.ac.uk>
4a53940 Initial version
eb authored
8 Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/
82c30e6 @gwern +cabal metadata
gwern authored
9 Stability: experimental
e2cda23 Fixing conflicts, merging in gwern's patches
eb authored
10 Build-depends: base, haskell98, parsec, mtl, directory, containers
4a53940 Initial version
eb authored
11 Extensions: MultiParamTypeClasses, FunctionalDependencies,
12 ExistentialQuantification, OverlappingInstances
ec67c2c Record pattern match totality
eb authored
13 Category: Theorem provers, Dependent Types
82c30e6 @gwern +cabal metadata
gwern authored
14 Synopsis: Theorem proving library based on dependent type theory
384098f update cabal
eb authored
15 Description: Ivor is a type theory based theorem prover, with a
16 Haskell API, designed for easy extending and embedding
17 of theorem proving technology in Haskell
18 applications. It provides an implementation of the
19 type theory and tactics for building terms, more or
20 less along the lines of systems such as Coq or Agda,
21 and taking much of its inspiration from Conor
22 McBride's presentation of OLEG.
491515a @gwern rearrange cabal fields
gwern authored
23 .
384098f update cabal
eb authored
24 The API provides a collection of primitive tactics and
25 combinators for building new tactics. It is therefore
26 possible to build new tactics to suit specific
27 applications. Ivor features a dependent type theory
28 similar to Luo's ECC with definitions (and similar to
29 that implemented in Epigram), with dependent pattern
30 matching, and experimental multi-stage programming
31 support. Optionally, it can be extended with
8ea14a0 Sneakily changed version numbering
eb authored
32 heterogeneous equality, primitive types and operations,
384098f update cabal
eb authored
33 new parser rules, user defined tactics and (if you
34 want your proofs to be untrustworthy) a fixpoint
35 combinator.
491515a @gwern rearrange cabal fields
gwern authored
36
16c6321 @gwern goodness. That left all the docs and examples out
gwern authored
37 Data-files: BUGS, INSTALL, TODO, docs/macros.ltx, docs/local.ltx, docs/tt.tex, docs/conclusion.tex,
38 docs/intro.tex, docs/hcar.sty, docs/tactics.tex, docs/library.ltx,
39 docs/shell.tex, docs/dtp.bib, docs/HCAR.tex, docs/Makefile,
40 docs/combinators.tex, docs/humett.tex, docs/interface.tex,
41 papers/tutorial/tutorial.tex, papers/tutorial/macros.ltx, papers/tutorial/theoremproving.tex,
42 papers/tutorial/introduction.tex, papers/tutorial/hslibrary.tex, papers/tutorial/library.ltx,
43 papers/tutorial/programming.tex, papers/tutorial/Makefile, papers/bib/literature.bib,
44 papers/ivor/examples.tex, papers/ivor/code.tex, papers/ivor/macros.ltx,
45 papers/ivor/ivor.tex, papers/ivor/corett.tex, papers/ivor/conclusions.tex,
46 papers/ivor/intro.tex, papers/ivor/llncs.cls, papers/ivor/tactics.tex,
47 papers/ivor/library.ltx, papers/ivor/dtp.bib, papers/ivor/alink.bib,
adc1f0e Use cabal directory for prefix
eb authored
48 papers/ivor/Makefile, papers/ivor/embounded.bib,
49 lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,
50 lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt
51
16c6321 @gwern goodness. That left all the docs and examples out
gwern authored
52
53 Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, examplett/partial.tt, examplett/nat.tt,
54 examplett/vec.tt, examplett/lt.tt, examplett/Test.hs, examplett/plus.tt,
55 examplett/jmeq.tt, examplett/eq.tt, examplett/logic.tt, examplett/interp.tt,
56 examplett/stageplus.tt, examplett/Nat.hs, examplett/general.tt, examplett/natsimpl.tt,
57 examplett/test.tt, examplett/vect.tt, examplett/fin.tt, examplett/ack.tt,
adc1f0e Use cabal directory for prefix
eb authored
58 IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs
16c6321 @gwern goodness. That left all the docs and examples out
gwern authored
59
60
61
975e1a8 Added some Data.Binary serialisation
eb authored
62 Build-depends: base >=3 && <5, parsec, mtl, directory, binary
491515a @gwern rearrange cabal fields
gwern authored
63 Build-type: Simple
64
82c30e6 @gwern +cabal metadata
gwern authored
65 Extensions: MultiParamTypeClasses, FunctionalDependencies,
203a435 Remove -fglasgow-exts
eb authored
66 ExistentialQuantification, OverlappingInstances,
67 TypeSynonymInstances, PatternGuards
491515a @gwern rearrange cabal fields
gwern authored
68 -- Needs some -Wall cleanup
69 -- GHC-options: -Wall
70
4a53940 Initial version
eb authored
71 Exposed-modules:
491515a @gwern rearrange cabal fields
gwern authored
72 Ivor.TT, Ivor.Shell, Ivor.Primitives,
8ec5e55 Added split tactic
eb authored
73 Ivor.TermParser, Ivor.ViewTerm, Ivor.Equality,
7c68bad Reinstated plugins
eb authored
74 Ivor.Plugin, Ivor.Construction
491515a @gwern rearrange cabal fields
gwern authored
75 Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State,
2a5fab1 Started on new evaluator
eb authored
76 Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator
0ad8193 Lifted values into Ivor.Values
eb authored
77 Ivor.Gadgets, Ivor.SC, Ivor.Bytecode, Ivor.Values,
4a53940 Initial version
eb authored
78 Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
79 Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
80 Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,
adc1f0e Use cabal directory for prefix
eb authored
81 Ivor.RunTT, Ivor.Compiler, Ivor.Errors,
337b24a Stared Overloading (not yet working...)
eb authored
82 Ivor.PatternDefs, Ivor.ShellState, Ivor.Scopecheck,
adc1f0e Use cabal directory for prefix
eb authored
83 Ivor.Overloading,
84 Paths_ivor
Something went wrong with that request. Please try again.