Demo.v « theories « tuto0 « plugin_tutorial « doc - coq - The formal proof system

about summary refs log tree commit diff

path: root/doc/plugin_tutorial/tuto0/theories/Demo.v

blob: bdc61986af794afc58e02a25f7550304fc1d01fb (plain)

From Tuto0 Require Import Loader.

HelloWorld.

Lemma test : True.
Proof.
hello_world.
Abort.