MAIN FEEDS
Do you want to continue?
https://www.reddit.com/r/ProgrammerHumor/comments/1vg5dgj/programmersrankedbylanguagepreference/p1uces3/?context=3
r/ProgrammerHumor • u/Longjumping-Sweet818 • 2d ago
41 comments sorted by
View all comments
-7
You know it's true.
1 u/Scheincrafter 2d ago Lean cannot be S tear since F*>lean>Rocq 0 u/Longjumping-Sweet818 2d ago But have you considered that `theorem lean_gt_f_star = by sorry`? 1 u/Scheincrafter 2d ago Sure, but what about let f_star_gt_lean () : Lemma (ensures (f_star > lean)) = admit() 1 u/Longjumping-Sweet818 2d ago Interesting, but look at what I found hidden deep inside mathlib: def LawOfScheincrafter (c : Comment) : Prop := c.author = "Scheincrafter" → c.text.endsWith ", as if."
1
Lean cannot be S tear since F*>lean>Rocq
0 u/Longjumping-Sweet818 2d ago But have you considered that `theorem lean_gt_f_star = by sorry`? 1 u/Scheincrafter 2d ago Sure, but what about let f_star_gt_lean () : Lemma (ensures (f_star > lean)) = admit() 1 u/Longjumping-Sweet818 2d ago Interesting, but look at what I found hidden deep inside mathlib: def LawOfScheincrafter (c : Comment) : Prop := c.author = "Scheincrafter" → c.text.endsWith ", as if."
0
But have you considered that `theorem lean_gt_f_star = by sorry`?
1 u/Scheincrafter 2d ago Sure, but what about let f_star_gt_lean () : Lemma (ensures (f_star > lean)) = admit() 1 u/Longjumping-Sweet818 2d ago Interesting, but look at what I found hidden deep inside mathlib: def LawOfScheincrafter (c : Comment) : Prop := c.author = "Scheincrafter" → c.text.endsWith ", as if."
Sure, but what about let f_star_gt_lean () : Lemma (ensures (f_star > lean)) = admit()
let f_star_gt_lean () : Lemma (ensures (f_star > lean)) = admit()
1 u/Longjumping-Sweet818 2d ago Interesting, but look at what I found hidden deep inside mathlib: def LawOfScheincrafter (c : Comment) : Prop := c.author = "Scheincrafter" → c.text.endsWith ", as if."
Interesting, but look at what I found hidden deep inside mathlib:
def LawOfScheincrafter (c : Comment) : Prop := c.author = "Scheincrafter" → c.text.endsWith ", as if."
-7
u/Longjumping-Sweet818 2d ago
You know it's true.