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.

Sign up for GitHub

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

Jump to bottom

Some code related to Cubical Agda runs also when the K rule is on #5760

Closed
nad opened this issue Jan 29, 2022 · 1 comment
Closed

Some code related to Cubical Agda runs also when the K rule is on #5760

nad opened this issue Jan 29, 2022 · 1 comment
Assignees
@nad
Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp performance Slow type checking, interaction, compilation or execution of Agda programs type: enhancement Issues and pull requests about possible improvements
Milestone
2.6.3

Comments

@nad
Copy link
Contributor

nad commented Jan 29, 2022

I suppose that it would make sense to not run the following code when the K rule is on:

agda/src/full/Agda/TypeChecking/Rules/Data.hs

Lines 188 to 189 in 798be60

mtranspix <- inTopContext $ defineTranspIx name
transpFun <- inTopContext $ defineTranspFun name mtranspix cons (dataPathCons dataDef)

@Saizan, do you agree?
@nad nad added type: enhancement Issues and pull requests about possible improvements performance Slow type checking, interaction, compilation or execution of Agda programs cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp labels Jan 29, 2022
@nad nad added this to the 2.6.3 milestone Jan 29, 2022
@Saizan
Copy link
Contributor

Saizan commented Jan 30, 2022

Yes, I agree.

nad added a commit that referenced this issue Feb 4, 2022
@nad
Fixed #5760.
ef7c52c
@nad nad self-assigned this Feb 4, 2022
@nad nad closed this as completed in 9911f73 Feb 4, 2022
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nad nad

Labels
cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp performance Slow type checking, interaction, compilation or execution of Agda programs type: enhancement Issues and pull requests about possible improvements
Projects
None yet
Milestone
2.6.3
Development

No branches or pull requests
2 participants
@Saizan @nad