Something went wrong. Try again.
an experimental forester forest with a proof assistant bolted on
Something went wrong. Try again.
189 B · 14 lines
at main
1234567891011121314\import{holbert-macros}\title{Even Numbers}\taxon{Definition} \hol/induct{evens}{ \hol/dep{config}{config}}{ ---- E-Z (Even 0) n. (Even n) ------- E-SS (Even (S (S n)))}