Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Module Parameters public or private? #1237

Closed
weaversa opened this issue Jul 18, 2021 · 2 comments · Fixed by #1559
Closed

Module Parameters public or private? #1237

weaversa opened this issue Jul 18, 2021 · 2 comments · Fixed by #1559
Assignees
Labels
parameterized modules Related to Cryptol's parameterized modules

Comments

@weaversa
Copy link
Collaborator

In the recent past (just a few months ago), parameterized module parameters have been public, by which I mean that if I instantiated a parameterized module, module parameters were in scope in the REPL. However, it seems they are now private (no longer in scope in the REPL).

Two things, I guess...1) I don't see this behavior documented. 2) What is the right thing to do here?

@weaversa
Copy link
Collaborator Author

Maybe the real issue is not private vs. public, but whether private definitions are accessible in the REPL for an instantiation of a parameterized module -- which I think should be yes (if only to facilitate development&testing). I agree that the parameters themselves should be private (not pollute the namespace of child modules).

@robdockins robdockins added the parameterized modules Related to Cryptol's parameterized modules label Jul 20, 2021
@qsctr
Copy link
Contributor

qsctr commented Jul 27, 2023

This will be fixed as part of #1455 (the parameters will be accessible at the REPL, along with other things defined in the functor).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parameterized modules Related to Cryptol's parameterized modules
Projects
None yet
3 participants