Skip to content

Instantly share code, notes, and snippets.

@maonus
Created October 8, 2020 00:50
Show Gist options
  • Save maonus/9ed54f15dc0c66834c94b607be5657b9 to your computer and use it in GitHub Desktop.
Save maonus/9ed54f15dc0c66834c94b607be5657b9 to your computer and use it in GitHub Desktop.
#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))
@wilbowma
Copy link

wilbowma commented Oct 9, 2020

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?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment