ucsd-formalconstrained-decoding-formalization0.1.0

Formalization of a grammar-constrained decoding algorithm in Lean.
Sort by
  1. Git dependency.
    Found on Reservoir.

    replv4.29.0-rc6

    A simple REPL for Lean 4, returning information about errors and sorries.
  2. Git dependency.
    Found on Reservoir.

    lean4exportv4.29.0-rc6

    Plain-text declaration export for Lean 4
  3. Registry dependency.
    Found on Reservoir.

    mathlib5a2fd49

    The math library of Lean 4