Something went wrong. Try again.
the next generation of the in-browser educational proof assistant
Something went wrong. Try again.
624 B · 29 lines
at main
123456789101112131415161718192021222324252627282930\import{holbert-macros}\title{Proofs!}\taxon{Theorem}\p{All [even](evens) numbers are natural numbers. Note that [even numbers](evens) are defined in a separate page, but changes are seamlessly synced over. }\hol/proof{evensarenats}{ \hol/dep{hng-0000}{config} \hol/dep{hng-0000}{notation} \hol/dep{nats}{nat} \hol/dep{evens}{evens} }{ x. (x Even) ---------------- f (x Nat) x. asm |- ?} \hol/proof{natinversion}{ \hol/dep{hng-0000}{config} \hol/dep{hng-0000}{notation} \hol/dep{nats}{nat} }{ x. ((@S x) Nat) ---------------- S-inv (x Nat) x. asm |- ?}