Skip to content

Instantly share code, notes, and snippets.

@aymanosman

aymanosman/use-cur-example.rkt

Created February 23, 2020 20:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save aymanosman/4777386958510a8213361151b1f12b97 to your computer and use it in GitHub Desktop.
Save aymanosman/4777386958510a8213361151b1f12b97 to your computer and use it in GitHub Desktop.
Download ZIP
Example of using Cur
Raw
use-cur-example.rkt
#lang cur
(require cur/ntac/base
cur/ntac/standard
cur/ntac/rewrite
cur/stdlib/sugar
cur/stdlib/nat
cur/stdlib/equality)
((ntac
(∀ [x : Nat] [y : Nat]
(-> (== Nat x y)
(== Nat y x)))
(by-intros x y x=y)
; define local thm named y=x
(by-assert y=x (== Nat y x))
; prove y=x
display-focus
(by-rewriteR x=y)
display-focus
reflexivity
; prove original goal using y=x
display-focus
(by-assumption y=x))
1 1 (refl Nat 1))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment