Skip to content

Instantly share code, notes, and snippets.

@tangentstorm

tangentstorm/proof

Last active Aug 29, 2015
Embed
What would you like to do?
a proof language (embedded in nial)
r0 := ("^^>^* (ph 'exponent rule')
(("$x "^ "$y) "^ "$z)
"= (("$x "^ ("$y "* "$z))))
r1 := ("xy>yx (ph 'commutative rule for *')
("x "* "y)
"= ("y "* "x))
p := (("x "^ "y) "^ "z);
q := (("x "^ "z) "^ "y);
t := { show p "= q (
(("x "^ "y) "^ "z) "| "r0
"= ("x "^ ("y "* "z)) "| "r1
"= ("x "^ ("z "* "y)) "| "_r
"= (("x "^ "z) "^ "y) ) }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment