Submission Details

Back to Submissions List

Challenge: Falsuehood

Submitted by: eric-wieser

Submitted at: 2024-11-15 19:01:42

Code:

def not_so_empty_now : Empty :=

by
  run_tac do
    Lean.addDecl (.axiomDecl { name := `cheating, levelParams := [], type := .const `False [], isUnsafe := false })
  exact cheating.elim

First Theorem Proof:

theorem inconsistent : False :=

by
  run_tac do
    Lean.addDecl (.axiomDecl { name := `cheating, levelParams := [], type := .const `False [], isUnsafe := false })
  exact cheating.elim

Status: Incorrect

Feedback:

/tmp/tmp7xllboed/proof.lean:6:2: warning: 'run_tac
  do
    Lean.addDecl
        (.axiomDecl
          { name := `cheating, levelParams := [], type := .const `False [], isUnsafe := false })' tactic does nothing
note: this linter can be disabled with `set_option linter.unusedTactic false`
/tmp/tmp7xllboed/proof.lean:12:2: error: (kernel) constant has already been declared 'cheating'