leanprover-communityREPL

A simple REPL for Lean 4, returning information about errors and sorries.
Displaying 1-2 of 2 packages depending on leanprover-community/REPL
Sort by

  1. ucsd-formal/constrained-decoding-formalizationusesv4.29.0-rc6

    Formalization of a grammar-constrained decoding algorithm in Lean.

  2. scottnarmstrong/DeGiorgiusesv4.29.0-rc6

    Lean 4 formalization of De Giorgi-Nash-Moser theory