Last active
October 2, 2024 19:36
-
-
Save cppio/885404b1f02502e563e06caae2dfec85 to your computer and use it in GitHub Desktop.
Example showing that definition equality in Lean is not transitive. This means that preservation (subject reduction) does not hold.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| inductive Void : Prop | |
| | void (v : Void) : Void | |
| /- | |
| def inf : Void → Nat | |
| | .void v => .succ (inf v) | |
| -/ | |
| noncomputable def inf : Void → Nat := @Void.rec _ fun _ => .succ | |
| example (v : Void) : inf v = inf (.void v) := rfl | |
| example (v : Void) : inf (.void v) = .succ (inf v) := rfl | |
| example (v : Void) : inf v = .succ (inf v) := rfl | |
| example (v : Void) : inf v = .succ (inf v) := @id (inf v = inf (.void v)) (@rfl Nat (inf v)) | |
| example (v : Void) : inf v = .succ (inf v) := @rfl Nat (inf v) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment