Skip to main content

Questions tagged [module]

Module generally refers to a logical subdivision of the whole program.

Filter by
Sorted by
Tagged with
0 votes
0 answers
9 views

How do I fold a function over the bindings in a map in Isabelle?

Coq has the FMap modules, is there a similar Isabelle theory module? https://coq.inria.fr/doc/v8.19/stdlib/Coq.FSets.FMapInterface.html What I want to be able to do is fold a function over the ...
Glyn Webster's user avatar
2 votes
0 answers
43 views

A module signature is silently changed when it is imported. Its `eq_dec` lemma has its `=` operator changed to `eq` and no longer works

This following works as I'd expect it to. But if I place the TypeDef_S signature in another file then the apply typeDef.eq_dec. ...
Glyn Webster's user avatar
2 votes
1 answer
142 views

Is there a way to rename parameters when including/reusing a module type in Coq?

Say I have a (more general) module type Collection that specifies some operations like read and write and now I want to create (more specialized) module types like <...
C.E.Sally's user avatar
  • 121
2 votes
1 answer
77 views

What is the correct way to define a DecidableType module?

I have this type in Coq: Inductive s_symb : Type := | s_symb_expr : nat -> s_symb | s_symb_fld : nat -> list string -> s_symb. I want to create a ...
Pietro Braione's user avatar
4 votes
1 answer
107 views

Universe polymorphism and modules in Coq

The following code (without universe polymorphism) is accepted by Coq (8.16.0) : ...
Dave's user avatar
  • 175
7 votes
1 answer
107 views

Why Coq's `Include` is designed to instantiate functor with current interactive defining module?

It is surprising for me to see that Coq can Include a functor and will instantiate it with the current interactive module. Coq Ref Manual: Command Include ...
Ende Jin's user avatar
  • 429
6 votes
1 answer
151 views

Does Coq's Module and Functor type-check incrementally?

I am trying to search the following questions online but I failed: When applying a functor (parametrized module), will the contents inside the functor be re-type-checked? Will Coq's command ...
Ende Jin's user avatar
  • 429