From c32cdee4f7ddc03138d06ed65ae8cd588c37243c Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Mon, 8 Dec 2025 21:49:05 -0300 Subject: [PATCH] Format, --- rocq-demo/rocq_playground.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rocq-demo/rocq_playground.v b/rocq-demo/rocq_playground.v index ede2f71..9365870 100644 --- a/rocq-demo/rocq_playground.v +++ b/rocq-demo/rocq_playground.v @@ -1,11 +1,11 @@ (* SPDX-License-Identifier: LGPL-3.0-or-later See Notices.txt for copyright information *) -(* This file demonstrates converting simple HDL designs into Rocq, as well +(** This file demonstrates converting simple HDL designs into Rocq, as well as proofs by induction that parallels those of formal verification in Symbiyosys with the "smtbmc" engine in the "prove" mode. *) -(* Models a simple register, feeding back to itself. We prove that, +(** Models a simple register, feeding back to itself. We prove that, when initialized to zero, it stays always at zero. *) Module simple_register.