Submission Details

Back to Submissions List

Challenge: Falsuehood

Submitted by: eric-wieser

Submitted at: 2024-11-15 19:02:16

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 :=

cheating

Status: Correct

Feedback:

/tmp/tmpjs2g24qv/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`