agda icon indicating copy to clipboard operation
agda copied to clipboard
verified publisher icon agda

Add 4 reflection primitives of the form `ask*` and `with*`

Open WhatisRT opened this issue 3 years ago • 5 comments

The asterisk ranges over Reconstructed, Normalisation, ExpandLast and ReduceDefs. withReconstructed and withNormalisation replace their old counterparts, and onlyReduceDefs and dontReduceDefs have been removed.

WhatisRT avatar May 09 '22 19:05 WhatisRT

It seems that our PR (#5978) breaks yours but I have merged ours into the master branch.

I'd like to merge yours soon as well. If you don't have time to resolve conflicts, I will try to get this through myself.

L-TChen avatar Aug 25 '22 07:08 L-TChen

@WhatisRT or @L-TChen: We're planning to release Agda 2.6.3 by the end of October, do you think you have time to work on updating this PR before then? If not, please bump the milestone to 2.6.4.

jespercockx avatar Aug 31 '22 14:08 jespercockx

@WhatisRT or @L-TChen: We're planning to release Agda 2.6.3 by the end of October, do you think you have time to work on updating this PR before then? If not, please bump the milestone to 2.6.4.

I think I can make it as I will have some time after mid October.

L-TChen avatar Sep 03 '22 06:09 L-TChen

I don't think we should add new features right before the release.

nad avatar Sep 05 '22 10:09 nad

Ok, then perhaps it's best to push this to 2.6.4 and merge it right after the release.

jespercockx avatar Sep 05 '22 10:09 jespercockx

@L-TChen could you bring this PR back up to date so it can be merged?

jespercockx avatar Jan 03 '23 14:01 jespercockx

I rebased @WhatisRT's change on the current master branch and solved conflicts. But I don't know how to (force) push my change to his branch. May @WhatisRT can have a look and update his branch?

https://github.com/agda/agda/compare/master...L-TChen:agda:tc-reader-primitives

L-TChen avatar Jan 17 '23 09:01 L-TChen

I rebased @WhatisRT's change on the current master branch and solved conflicts. But I don't know how to (force) push my change to his branch. May @WhatisRT can have a look and update his branch?

master...L-TChen:agda:tc-reader-primitives

Try git fetch origin refs/pull/$1/head:pr/$1 && git checkout pr/$1 where $1=5898, should work provided you have the access rights.

omelkonian avatar Jan 17 '23 09:01 omelkonian

@L-TChen Thank you, I'll update the branch!

WhatisRT avatar Jan 17 '23 11:01 WhatisRT

This commit has been merged from the corresponding branch on agda/agda directly by https://github.com/agda/agda/pull/6443 instead.

L-TChen avatar Jan 18 '23 15:01 L-TChen