CODEWITHSUNDEEP
coq
Quyen
Quyen

Reputation: 1373

How to use the Lemma inside a module in Coq?

I defined a module type in one file called A.v

Module Type WeakPair.
...

End WeakPair.

Module WeakPairProps (Import WP : WeakPair).

 Lemma Weak_A ....

End WeakPairProps.

Then I want to define another file B.v that can use the Lemma in WeakPairProps for example : Weak_A. Because WeakPairProps is not a module type so I do not know how to write a module that can reuse the lemma in WeakPairProps.

Upvotes: 0

Views: 214

Answers (1)

Ptival
Ptival

Reputation: 9437

First you need to define a module that implements the module type WeakPair :

Module WeakPairImpl <: WeakPair.
(* stuff goes here *)
End WeakPairImpl.

Now you can instantiate the functor WeakPairProps:

Module WeakPairPropsInst := WeakPairProps(WeakPairImpl).

You are now able to refer to the lemma:

WeakPairPropsInst.lemma

You can import WeakPairPropsInst if you desire not to use qualified names.

Upvotes: 2

Related Questions