Submission Details

Back to Submissions List

Challenge: Falsehood

Submitted by: blizzard_inc

Submitted at: 2024-11-15 18:06:25

Code:

universe u
axiom ignore: PEmpty.{u}

def not_so_empty_now: Empty

:= ignore.elim.{0}

First Theorem Proof:

theorem inconsistent : not_so_empty_now -> False

:= ignore.elim.{0}

Status: Incorrect

Feedback:

/tmp/tmpi7_kguip/proof.lean:10:23: error: type expected, got
  (not_so_empty_now : Empty)