proofs-are-memes.rkt

#lang cur

(require
 cur/stdlib/nat
 cur/stdlib/equality
 cur/ntac/base
 cur/ntac/standard)

(define-syntax hot-take (make-rename-transformer #'define-theorem))
(define-syntax unpopular-opnion (make-rename-transformer #'define-theorem))
(begin-for-syntax
  (require (for-syntax racket/base))
  (define-syntax dont-|@|-me (make-rename-transformer #'qed)))


(hot-take my-spicy-take
          (forall (a : Nat) (b : Nat) (c : Nat)
                  (== Nat (plus a (plus b c)) (plus (plus a b) c)))
          dont-|@|-me)