hcomp symbols in interface not hidden under --cubical-compatible · Issue #7048 · agda/agda · GitHub

8000 hcomp symbols in interface not hidden under --cubical-compatible · Issue #7048 · agda/agda · GitHub

More Web Proxy on the site http://driver.im/

hcomp symbols in interface not hidden under --cubical-compatible #7048

Closed

Closed

hcomp symbols in interface not hidden under --cubical-compatible#7048

Assignees

Labels

cubical-compatibleinterfacetype: bug

Milestone

From #7044 (comment):

When printing the signatures of the interface, I see Inner.hcomp-T. Why is that generated without --cubical-compatible?

Test case:

module Inner where

data T : Set where
  t : T

Running

agda-quicker Inner.agda -v 5 | grep hcomp

shows that cubical-related code is executed:

Generated name: [...] "hcomp-T" [...]

Metadata

Assignees

andreasabel

Labels

cubical-compatibleinterfacetype: bug

Type

No type

Projects

No projects

Milestone

2.6.4.2

Relationships

None yet

Development

No branches or pull requests

0