Skip to content

Commit

Permalink
[ #1063 ] Document Agda's new behaviour
Browse files Browse the repository at this point in the history
  • Loading branch information
@jespercockx
jespercockx committed Dec 4, 2018
1 parent ec6d15f commit d57465a
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions CHANGELOG.md
View file
Expand Up @@ -214,6 +214,12 @@ Type checking and interaction
instance constructor tt
```

* Metavariables created in the (types of) module parameters are only
frozen at the end of that module (see Issue
[#1063](https://github.com/agda/agda/issues/1063)). Previously, Agda
would freeze these metavariables after the first declaration in the
module.

Pragmas and options
-------------------

Expand Down

5 comments on commit d57465a

@nad
Copy link
Contributor

@nad nad commented on d57465a Dec 4, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this comment correct also for modules inside mutual blocks?

A : Set₁

module _ (B : Set _) where

A = Set

@jespercockx
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know, feel free to change it if you think it's incorrect.

@nad
Copy link
Contributor

@nad nad commented on d57465a Dec 5, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the meta-variable in the module telescope that I gave above frozen at the end of the module or at the end of the mutual block? (I suppose I could try to construct an example that would let me figure out the answer myself.)

@jespercockx
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Based on my understanding of the code, metas are only frozen when we're not in a mutual block. So if we are in a mutual block, metas of module parameters will stay open for the whole mutual block.

@nad
Copy link
Contributor

@nad nad commented on d57465a Dec 5, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I edited the text.

Please sign in to comment.