latte.core
This namespace provides the top-level forms of the LaTTe framework.
This namespace provides the top-level forms of the LaTTe framework.
assumecljmacro
(assume params & body)An assume step of the form (assume [x1 T1 x2 T2 ...] <body>).
An assume step of the form `(assume [x1 T1 x2 T2 ...] <body>)`.
defaxiomcljmacro
(defaxiom & args)Declaration of an axiom of the form:
(defaxiom <name>
"<docstring>"
[[x1 T1] ... [xN TN]] ;; <params>
<body>)
with the specified name (first argument)
an optional docstring (second argument), a vector params of parameters
and the axiom body, the axiom statement as a lambda-term (last argument).
Each parameter is a pair [x T] with x the parameter name and T its
type.
An axiom is accepted without a proof, and should thus be used with extra care. The LaTTe rule of thumb is that theorems should be favored, but axioms are sometimes required (e.g. the law of the excluded middle) or more "reasonable" because of the proof length or complexity. In all cases the introduction of an axiom must be justified with strong (albeit informal) arguments.
Declaration of an axiom of the form:
(defaxiom <name>
"<docstring>"
[[x1 T1] ... [xN TN]] ;; <params>
<body>)
with the specified `name` (first argument)
an optional `docstring` (second argument), a vector `params` of parameters
and the axiom `body`, the axiom statement as a lambda-term (last argument).
Each parameter is a pair `[x T]` with `x` the parameter name and `T` its
type.
An axiom is accepted without a proof, and should thus be used with
extra care. The LaTTe rule of thumb is that theorems should be
favored, but axioms are sometimes required (e.g. the law of the excluded
middle) or more "reasonable" because of the proof length or complexity.
In all cases the introduction of an axiom must be justified with strong
(albeit informal) arguments.definitioncljmacro
(definition & args)Defines a mathematical term with the following structure:
(definition <name>
"<docstring>"
[[x1 T1] ... [xN TN]] ;; <params>
<body>)
composed of a name, and optional (but highly recommended)
docstring, a vector params of parameters (typed variables) and
body (a lambda-term) as definitional content.
An ex-info exception is thrown if the term cannot be defined.
Note that a definition is a def in the Clojure sense, the term is defined in the namespace where the definition
form is invoked.
Defines a mathematical term with the following structure:
(definition <name>
"<docstring>"
[[x1 T1] ... [xN TN]] ;; <params>
<body>)
composed of a `name`, and optional (but highly recommended)
`docstring`, a vector `params` of parameters (typed variables) and
`body` (a lambda-term) as definitional content.
An `ex-info` exception is thrown if the term cannot be defined.
Note that a definition is a `def` in the Clojure sense, the term is defined in the namespace where the `definition`
form is invoked.deflemmacljmacro
(deflemma & args)Declaration of a lemma, i.e. an auxiliary theorem. In LaTTe a lemma
is private. To export a theorem the defthm form must be used instead.
Otherwise the two forms are the same.
Declaration of a lemma, i.e. an auxiliary theorem. In LaTTe a lemma is private. To export a theorem the [[defthm]] form must be used instead. Otherwise the two forms are the same.
defnotationcljmacro
(defnotation & args)Defines a new notation, which is a function called at parsing time. The result must be pair [status u]
with status either :ok (parsing successful) with u the term generated by the notation,
or :ko (parsing failed) and u is the error, a map with at least a key :msg explaining
the failure.
Be careful that the parser will be called recursively on the generated term, hence recursive definitions must be handled with great care.
Defines a new notation, which is a function called at parsing time. The result must be pair `[status u]` with `status` either `:ok` (parsing successful) with `u` the term generated by the notation, or `:ko` (parsing failed) and `u` is the error, a map with at least a key `:msg` explaining the failure. Be careful that the parser will be called recursively on the generated term, hence recursive definitions must be handled with great care.
defthmcljmacro
(defthm & args)Declaration of a theorem of the following form:
(defthm <name>
"<docstring>"
[[x1 T1] ... [xN TN]] ;; <params>
<body>)
with the specified name (first argument)
an optional docstring (second argument), a vector params of parameters
and the theorem proposition as body (last argument).
Each parameter is a pair [x T] with x the parameter name and T its
type.
A theorem declared must later on be demonstrated using the proof form.
As a side effect, the statement of the theorem is recorded in the current
namespace (i.e. it is a Clojure def).
Declaration of a theorem of the following form:
(defthm <name>
"<docstring>"
[[x1 T1] ... [xN TN]] ;; <params>
<body>)
with the specified `name` (first argument)
an optional `docstring` (second argument), a vector `params` of parameters
and the theorem proposition as `body` (last argument).
Each parameter is a pair `[x T]` with `x` the parameter name and `T` its
type.
A theorem declared must later on be demonstrated using the [[proof]] form.
As a side effect, the statement of the theorem is recorded in the current
namespace (i.e. it is a Clojure `def`).examplecljmacro
(example & args)An example of the form (example T <steps>) is the statement of a proposition, as a type T,
as well as a proof.
An example of the form `(example T <steps>)` is the statement of a proposition, as a type `T`, as well as a proof.
forallclj
(forall params body)The universal quantifier (forall [x A] t) is ∀x:A.t (or Πx:A.t in type theory).
As a syntactic sugar an expression of form (forall [x y z A] t)
translates to (forall [x A] (forall [y A] (forall [z A] t)))
The universal quantifier `(forall [x A] t)` is ∀x:A.t (or Πx:A.t in type theory). As a syntactic sugar an expression of form `(forall [x y z A] t)` translates to `(forall [x A] (forall [y A] (forall [z A] t)))`
havecljmacro
(have have-name have-type by-kw have-term)A have step of the form (have <x> T :by e) checks that the
term e is of type T. If it is the case, then the fact is recorded
as a local definition named <x>. Otherwise an error is signaled.
The type T can be replaced by _ in which case is is inferred rather than checked.
The name <x> can be replaced by _ in which case no definition is recorded.
A have step of the form `(have <x> T :by e)` checks that the term `e` is of type `T`. If it is the case, then the fact is recorded as a local definition named `<x>`. Otherwise an error is signaled. The type `T` can be replaced by `_` in which case is is inferred rather than checked. The name `<x>` can be replaced by `_` in which case no definition is recorded.
lambdaclj
(lambda params body)The abstraction (lambda [x A] t) is λx:A.t.
As a syntactic sugar an expression of form (lambda [x y z A] t)
translates to (lambda [x A] (lambda [y A] (lambda [z A] t)))
The abstraction `(lambda [x A] t)` is λx:A.t. As a syntactic sugar an expression of form `(lambda [x y z A] t)` translates to `(lambda [x A] (lambda [y A] (lambda [z A] t)))`
posecljmacro
(pose pose-name pose-kw pose-term)A local definition (pose P := e) allows a proof to refer to term e under
the name P in a proof. This is equivalent to (have P _ :by e) (with the type of
e inferred).
A local definition `(pose P := e)` allows a proof to refer to term `e` under the name `P` in a proof. This is equivalent to `(have P _ :by e)` (with the type of `e` inferred).
proofclj
(proof thm-name & steps)Provides a proof of theorem named thm-name using the given proof steps.
Provides a proof of theorem named `thm-name` using the given proof `steps`.
qedcljmacro
(qed qed-term)A Qed step of the form (qed e) checks that the
term e allows to finish a proof in the current context.
An error is signaled if the proof cannot be concluded.
A Qed step of the form `(qed e)` checks that the term `e` allows to finish a proof in the current context. An error is signaled if the proof cannot be concluded.
termcljmacro
(term & args)Parse a LaTTe term at the top-level. A context can be provided
in the form of a serie of [var type] pairs before the actual term.
Parse a LaTTe term at the top-level. A context can be provided in the form of a serie of `[var type]` pairs before the actual term.
term-eq?cljmacro
(term-eq? & args)Checks if two terms t and u are equal in the sense of
having the "same" normal form (up-to alpha-conversion, the
safe renaming of bound variables.
A context can be provided
in the form of a serie of [var type] pairs before the actual term.
Checks if two terms `t` and `u` are equal in the sense of having the "same" normal form (up-to alpha-conversion, the safe renaming of bound variables. A context can be provided in the form of a serie of `[var type]` pairs before the actual term.
the-type-ofclj
Replaces the provided term by its inferred type.
Replaces the provided term by its inferred type.
try-examplecljmacro
(try-example & args)This is the same as example but without throwing exceptions.
This is the same as [[example]] but without throwing exceptions.
try-proofclj
(try-proof thm-name & steps)Provides a proof of theorem named thm-name using the given proof steps.
This version only checks if the proof is correct or not, use the proof function
for actually registering the proof.
Provides a proof of theorem named `thm-name` using the given proof `steps`. This version only checks if the proof is correct or not, use the [[proof]] function for actually registering the proof.
type-check?cljmacro
(type-check? & args)Check if a term t in of the specified type ty.
A context can be specified as with type-of.
Check if a term `t` in of the specified type `ty`. A context can be specified as with [[type-of]].
type-ofcljmacro
(type-of & args)Give the type of a term t in a context at the top-level.
To only parse the term use term.
Give the type of a term `t` in a context at the top-level. To only parse the term use [[term]].
cljdoc is a website building & hosting documentation for Clojure/Script libraries
× close