This repository provides LeanSSR: a SSReflect tactic DSL for Lean4. LeanSSR extends Coq/SSReflect's tactic DSL with various new DSL constructions and enhanced mechanism for computational reflection.
With elan
installed, lake build
should suffice.
To use the latest version of LeanSSR in a Lean 4 project, first add this package as a dependency. In your lakefile.lean
, add
require ssreflect from git "https://github.com/verse-lab/lean-ssr" @ "master"
Then run
lake update ssreflect
You also need to make sure that your lean-toolchain
file contains the same version of Lean 4 as LeanSSR's, and that your versions of LeanSSR's dependencies (currently only Batteries4
) match. THe project does not support version ranges at the moment.
You may also consider using a stable release of the framework by adding the following to your lakefile.lean
instead:
require ssreflect from git "https://github.com/verse-lab/lean-ssr" @ "v1.0"
Once LeanSSR is downloaded and compiler, the following test file should compile:
import Ssreflect.Lang
example {α : Type} : α → α := by
-- The following is equivalent to
-- intro x; trivial
move=> x//
- The paper Small Scale Reflection for the Working Lean User provides a brief tutorial on LeanSSR and documents its main features
- LeanSSR Wiki containts detailed technical documentation on LeanSSR tactics
You can find LeanSSR use case examples at Examples
folder