Stream: Coq users

Topic: Importing a library using NixOS

view this post on Zulip Guilherme Silva (Oct 26 2021 at 03:43):

I am trying to import and use this project https://github.com/uwplse/verdi/blob/master/systems/Counter.v running this command:

nix-shell --packages coq coqPackages.Verdi --run coqtop <<< "Import Verdi.Verdi."

Why is it not working?
I received this message:

Welcome to Coq 8.11.2 (January 1980)

Coq < Toplevel input, characters 0-19:
> Import Verdi.Verdi.
> ^^^^^^^^^^^^^^^^^^^
Error: Cannot find module Verdi.Verdi

Coq <

view this post on Zulip Karl Palmskog (Oct 26 2021 at 04:44):

You need to use:

Require Import Verdi.Verdi.

Last updated: Sep 15 2024 at 13:02 UTC