Skip to content

Releases: Volland/lean-elpi

Release list

v0.3.3

v0.3.3 Latest
Latest

Choose a tag to compare

View all tags
@github-actions github-actions released this 16 Oct 07:18
v0.3.3
237a475

Full Changelog: v0.3.2...v0.3.3

Assets 6
Loading

v0.3.2

v0.3.2

Choose a tag to compare

View all tags
@github-actions github-actions released this 15 Oct 19:04
v0.3.2
46ffbb4

Full Changelog: v0.3.1...v0.3.2

Loading

v0.3.1

v0.3.1

Choose a tag to compare

View all tags
@github-actions github-actions released this 15 Oct 19:01
v0.3.1
a8fb91c

Full Changelog: v0.3.0...v0.3.1

Loading

v0.3.0

v0.3.0

Choose a tag to compare

View all tags
@github-actions github-actions released this 15 Oct 10:28
v0.3.0
e45a283

Full Changelog: v0.2.0...v0.3.0

Loading

LeanElpi 0.2.0

LeanElpi 0.2.0

Choose a tag to compare

View all tags
@Volland Volland released this 15 Oct 08:22
v0.2.0
3e922e1

0.2.0 — 2026-10-15

Added

  • Lean/ELPI type bridge (lean-interop capability): elpi_data, elpi_extern (total, partial, many), #elpi_signature.
  • lean.env.indt and lean.add_inductive builtins (the Lean analogue of Coq-Elpi's coq.env.indt / coq.env.add-indt).
  • Book chapter "Sharing types between Lean and λProlog", blog post, design paper tg.md/papers/interop.md.
  • Package metadata (description, keywords, license, readme) for Lake and Reservoir.

Changed

  • deriving Elpi supports type parameters (ELPI type variables A, B, …) and nested occurrences.
  • Derived declarations are loaded before registered builtin signatures, so builtins can mention derived types.

Fixed

  • deriving Elpi failed on every recursive type.
Loading

LeanElpi 0.1.0

LeanElpi 0.1.0

Choose a tag to compare

View all tags
@Volland Volland released this 14 Oct 14:45
v0.1.0
154d236

First release: ELPI engine, constraints/CHR, Lean integration, and the LF layer with kernel-checked certificates. Use as a Lake dependency: require «lean-elpi» from git "https://github.com/Volland/lean-elpi" @ "v0.1.0".

Loading