# latte.core

This namespace provides the top-level forms of the LaTTe framework.

### *proof-certification-enabled*

#### dynamic

### assume

#### macro

`(assume params & body)`

An assume step of the form `(assume [x1 T1 x2 T2 ...] <body>)`

.

### defaxiom

#### macro

`(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.

### defimplicit

#### macro

`(defimplicit & args)`

### defimplicit*

#### macro

`(defimplicit* & args)`

### definition

#### macro

`(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.

### deflemma

#### macro

`(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.

### defnotation

#### macro

`(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.

### defthm

#### macro

`(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`

).

### example

#### macro

`(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.

### forall

`(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)))`

### have

#### macro

`(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.

### lambda

`(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)))`

### pose

#### macro

`(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).

### proof

`(proof thm-name & steps)`

Provides a proof of theorem named `thm-name`

using the given proof `steps`

.

### qed

#### macro

`(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.

### search-theorem

`(search-theorem patt)`

`(search-theorem where patt)`

Search a theorem using pattern `patt`

. A pattern (generally quoted) is either: - any clojure value, that has to be matched exactly, with the exception of a symbol starting with a question mark (denoting a variable) - a simple variable `?X`

that can match anything - a list/sequence of patterns `(patt1 patt2 ...)`

- a zero-or-many variable `?Y*`

that matches zero or more times greedily - a one-or-many variable `?Z+`

that matches at least once greedily - an optional variable `?V?`

that matches at most once The optional argument `where`

is the name (symbol) of a namespace where the search must be applied (by default, use all registered namespaces)

The special variables `?_`

, `?_*`

, `?_+`

and `?_?`

produce no binding when matched.

The result is a vector of matches, each match being a pair `[theorem-var match-env]`

with `theorem-var`

the reference to the theorem as a clojure var, and `match-env`

the variable bindings corresponding to the match.

### term

#### macro

`(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.

### term-eq?

#### macro

`(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.

### the-type-of

Replaces the provided term by its inferred type.

### try-proof

`(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.

### type-check?

#### macro

`(type-check? & args)`

Check if a term `t`

in of the specified type `ty`

. A context can be specified as with type-of.

### type-of

#### macro

`(type-of & args)`

Give the type of a term `t`

in a context at the top-level. To only parse the term use term.