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