Commit 2025-11-21 19:36 36a2b22f

View on Github ā†’

feat: extract_goal preserves explicit foralls (#31342)

  • feat: extract_goal preserves explicit foralls
  • fix: update goalSignature call for new return type The goalSignature function now returns a 4-tuple including a boolean for hasOriginalForalls. Update the destructuring pattern in TacticAnalysis/Declarations.lean to account for this new field. šŸ¤– Generated with Claude Code Co-Authored-By: Claude noreply@anthropic.com

Estimated changes

added theorem foralls_variants