Submission Details

Back to Submissions List

Challenge: Falsehood

Submitted by: blizzard_inc

Submitted at: 2024-11-15 18:05:04

Code:

universe u
axiom ignore: PEmpty.{u}

def not_so_empty_now: Empty

:= ignore.elim

First Theorem Proof:

theorem inconsistent : not_so_empty_now -> False

:= ignore.elim

Status: Incorrect

Feedback:

/tmp/tmpswxt59fl/code.lean:7:0: error: declaration 'not_so_empty_now' contains universe level metavariables at the expression
  PEmpty.elim.{1, ?u.5} ignore.{?u.5}
in the declaration body
  PEmpty.elim.{1, ?u.5} ignore.{?u.5}