Formalizing Dawn in Coq | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		Formalizing Dawn in Coq (danilafe.com)
		2 points by todsacerdoti on Nov 21, 2021 \| hide \| past \| favorite \| 1 comment

holonomically on Nov 21, 2021 [–]

Really nice tutorial on Coq's theorem proving facilities. It even covers Ltac which is rare for these kinds of tutorials.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact