Stream: Coq users

Topic: Library

view this post on Zulip zohaze (Apr 15 2023 at 06:14):

I have my own functions collection called all_value. When i call it, then am facing following problem
Require Export all_value.
I am using function "current" it appears as all_value.current a b=true . Want to look like
current a b=true .

view this post on Zulip Laurent Théry (Apr 15 2023 at 09:30):

Import all_value.

view this post on Zulip zohaze (Apr 15 2023 at 11:17):

Already i have "Require Export all_value". Now i have added "Require Import all_valu". But still every thing is same. No improvement.

view this post on Zulip Laurent Théry (Apr 15 2023 at 11:54):

What Coq says when you enter : 

Locate current.
Import all_value.
Locate current.

Last updated: Apr 20 2024 at 12:02 UTC