A very simple implementation of a little dependently typed language
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
AST.fs
Grammar.fsy
Induction.fs
Induction.fsi
LICENSE
Lexical.fsl
Makefile
Nat.fs
README
Result.fs
Toplevel.fs
Typechecker.fs
Utils.fs
getline.cs
prelude

README

This is a very simple and probably broken implementation of an as-yet-unnamed
dependently-typed language.

As of yet, it has only been developed with Mono running on Ubuntu, though
success has been reported in making it work with Mono on Mac OS X.  You will
probably have to modify the Makefile in order to get it to compile; in
particular, make sure to check the variable FSC for the name of your F#
compiler.

Additionally, the interpreter requires the .NET port of GNU getopt, which is
available from http://getopt.codeplex.com/ under the terms of the LGPL.

Please ensure that your terminal is set to use UTF-8.  The output from the
toplevel makes use of proper Π and λ symbols.

The file "prelude" contains the standard library and is read on startup.  See
this file for examples of syntax.

At the toplevel, any typed expression will be typechecked and evaluated.
Additionally, the following commands are available:

:quit         :q    Quit the toplevel.
:postulate    :p    Postulate a new opaque term inhabiting some type.
                    Example: :postulate Bool : Set
:showstate    :s    Show the contents of the global state (definitions).
:data               Define inductive datatypes.  For examples, see the file 'prelude'.
:define       :def  Define a new term in the global state.
                    Example: :def id := \T:Set.\x:T.x
:load         :l    Read the contents of a file, executing as if they were typed at
                    the toplevel.  Example: :l "prelude"
:debug              Toggle extended debugging printouts.


The syntax of terms generally follows ordinary conventions. However, to assist
in typing, "\" (backslash) can be used instead of "λ", "forall" can be used
instead of "Π", and "exists" can be used instead of "Σ".  Also, "A -> B" can
be written instead of Πx:A.B where x is not free in B.

The interpreter accepts the following command-line options:
--help          -h      Show the command-line help
--eval          -e      Evaluate the provided expression, then exit