---
title: "Checking Lean proofs in knitr documents"
output: rmarkdown::html_vignette
vignette: >
  %\VignetteIndexEntry{Checking Lean proofs in knitr documents}
  %\VignetteEngine{knitr::rmarkdown}
  %\VignetteEncoding{UTF-8}
---

```{r, include = FALSE}
knitr::opts_chunk$set(collapse = TRUE, comment = "#>")
library(leanknit)
# Use a disposable copy of the bundled example lake project so nothing is
# written into the installed package.
if (leanknit_available()) {
  options(leanknit.project = leanknit_example_project())
}
```

`leanknit` registers a `lean` knitr engine. A `lean` chunk is compiled and
checked against a `lake` project with `lake env lean`; its output is captured
below it. If no Lean toolchain is found (see `install_lean()`), chunks degrade
to a friendly notice so the document still renders.

```{r}
leanknit_available()
```

## Running Lean

Definitions accumulate across chunks within a session:

```{lean}
import LeanknitDemo

#eval (1 + 1 : Nat)
```

## Asserting the axiom base

The `axioms` chunk option appends `#print axioms <name>`. This puts the trust
base of a theorem in the rendered document — and, crucially, fails the render if
a `sorry` ever sneaks in. The bundled `one_add_one` is proved by `rfl`, so it
depends on nothing:

```{lean, axioms="LeanknitDemo.one_add_one"}
```

## Expected errors

A chunk marked `error=TRUE` shows the Lean error instead of aborting the render,
and does not poison later chunks in the session:

```{lean, error=TRUE}
theorem bogus : (1 : Nat) = 2 := rfl
```

## Why this matters

Because a failing check fails the render, a generated `.md`/`.html` cannot claim
a proof that does not actually hold. The document and the proof state cannot
drift apart.