meme.rkt

#lang cur
(require
  cur/stdlib/nat
  cur/stdlib/equality
  cur/ntac/base
  cur/ntac/standard
  cur/ntac/rewrite
  (for-syntax syntax/parse
              (for-syntax racket/base syntax/parse)))

(define-syntax unpopular
  (syntax-parser
    [(_ (~literal opinion)
        x ...)
     #`(define-theorem x ...)]))
(begin-for-syntax
  (define-syntax wat (make-rename-transformer #`display-focus))
  (define-syntax yeet (make-rename-transformer #`simpl))
  (define-syntax prove
    (syntax-parser 
      [(_ (~literal all)(~literal the)(~literal things))
       #`reflexivity]))
  (define-syntax yo
    (syntax-parser
      [(_ (~literal dawg)
          (~literal i)
          (~literal heard)
          (~literal you)
          (~literal like)
          b
          [is this a x 🦋] ...)
       #`(by-induction b #:as [x ...])]))
  (define-syntax i
    (syntax-parser
      [(_ (~literal put)
          (~literal a)
          b)
       #`(by-rewrite b)]))
  (define-syntax dont
    (syntax-parser
      [(_ (~literal @)
          (~literal me))
       #`qed])))
  
(unpopular opinion my-spicy-take
           (forall (a : Nat) (b : Nat) (c : Nat)
                   (== Nat (plus a (plus b c)) (plus (plus a b) c)))
           (by-intro a)
           (by-intro b) (by-intro c)
           yeet
           (yo dawg i heard you like a
               [is this a () 🦋]
               [is this a (n-1 proof-in-your-proof) 🦋])
           ;is this a z 🦋
           (prove all the things)
           ;is this a (suc a) 🦋
           (i put a proof-in-your-proof)
           yeet
           (prove all the things)
           (dont @ me))
     

At least 2 problems:

1. qed doesn't work like I remember, so it can't be used explicitly at the end. This is clearly a bug in cur
2. You're using ~literal instead of ~datum, which might be causing some binding issues?