Submission Details

Back to Submissions List

Challenge: Falsehood

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:30:59

Code:

universe u
axiom ignore: PEmpty.{u}

def not_so_empty_now: Empty

:= ignore

First Theorem Proof:

theorem inconsistent : not_so_empty_now -> False

:= by rintro ⟨⟩

Status: Incorrect

Feedback:

/tmp/tmpdi9svoke/code.lean:8:3: error: type mismatch
  ignore
has type
  PEmpty.{?u.4} : Sort ?u.4
but is expected to have type
  Empty : Type