Enforce compulsory Qed for Lean 4 #31
Description
Enforce proof in Lean 4 should end with a done tactic. This ensures that no underlying implementation bug can lead to accepting wrong proofs.
{{ message }}
Enforce proof in Lean 4 should end with a done tactic. This ensures that no underlying implementation bug can lead to accepting wrong proofs.