Code

Add proof validation to tactic mode#63

Code

Open

augustepoiroux wants to merge 3 commits intoleanprover-community:masterleanprover-community/repl:masterfrom augustepoiroux:proof_validationaugustepoiroux/repl:proof_validationCopy head branch name to clipboard

+367-59

Commits

Commits on Jan 8, 2025

• Initial fix (incomplete)

  augustepoiroux

  committed
  a02bae4

  Copy full SHA for a02bae4

• Add proofStatus field in ProofStepResponse + update tests

  augustepoiroux

  committed
  8562cf0

  Copy full SHA for 8562cf0

• Add a rootGoals option to instantiate synthetic sorries from declarations root goal

  Show description for f9dc2fb
  augustepoiroux

  committed
  f9dc2fb

  Copy full SHA for f9dc2fb