1lab/mikan
13
52
Fork
You've already forked mikan
9

Erase erasure #55

Closed
ncf wants to merge 1 commit from ncf/mikan:erase-erasure into main
pull from: ncf/mikan:erase-erasure
merge into: 1lab:main
1lab:main
1lab:aliao/occurs-opt
1lab:aliao/rec-con
1lab:fix-license
1lab:aliao/oopsie
1lab:aliao/strengthen-iapply
Owner
Copy link

Part of #1, removes erasure/quantities and some leftovers related to compilation.

Very WIP, I still need to fix the tests and docs (and figure out why Agda.Builtin.Cubical.Equiv is now failing).

Part of #1, removes erasure/quantities and some leftovers related to compilation. Very WIP, I still need to fix the tests and docs (and figure out why `Agda.Builtin.Cubical.Equiv` is now failing).
@ -567,3 +563,3 @@
-- To fix #7001, we could check whether the user has supplied the relevant modalities
-- (depending on which language flags are on), and refuse to progress if they are missing.
dontUseTargetType mayPostpone = ifM (pure mayPostpone `and2M` userOmittedModalities xs) postpone_ {-else-} do
dontUseTargetType mayPostpone = if mayPostpone then postpone_ else do
Owner
Copy link

this is why Equiv.agda is failing, there's an inferring lambda in there that got defaulted to I → _ because it was... annotated but not with modalities?

this is why `Equiv.agda` is failing, there's an inferring lambda in there that got defaulted to `I → _` because it was... annotated but not with modalities?
ncf marked this conversation as resolved
ncf force-pushed erase-erasure from 36b4329803
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 8e6252c62f
Some checks failed
ci/woodpecker/pr/test Pipeline failed
2026年04月29日 15:47:12 +02:00 Compare
ncf changed title from (削除) WIP: Erase erasure (削除ここまで) to Erase erasure 2026年04月30日 01:16:13 +02:00
ncf force-pushed erase-erasure from 69caca6793
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to c19fc2d7bb
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月02日 15:56:43 +02:00 Compare
ncf force-pushed erase-erasure from c19fc2d7bb
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 7a06782b5b
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月02日 17:13:43 +02:00 Compare
ncf changed title from (削除) Erase erasure (削除ここまで) to WIP: Erase erasure 2026年05月02日 17:14:06 +02:00
Author
Owner
Copy link

Rebased on top of #68.

Rebased on top of https://codeberg.org/1lab/mikan/pulls/68.
ncf force-pushed erase-erasure from 7a06782b5b
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to d8585f4fef
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月04日 23:41:08 +02:00 Compare
ncf changed title from (削除) WIP: Erase erasure (削除ここまで) to Erase erasure 2026年05月04日 23:41:34 +02:00

superceded by #70.

superceded by #70.
amyliao closed this pull request 2026年05月04日 23:43:59 +02:00
All checks were successful
ci/woodpecker/pr/test Pipeline was successful

Pull request closed

Please reopen this pull request to perform a merge.
Sign in to join this conversation.
No reviewers
Labels
Clear labels
1 - scope
language
 Backwards-compatible changes to the surface language, such as adding new features.
1 - scope
language change
 Breaking changes to a documented part of the surface language. These should be documented and specifically called out in the changelog.
1 - scope
performance
 Semantics-preserving performance work.
1 - scope
task
 Changes that are not apparent to the user, e.g. developer documentation and refactors, which do not need to be documented.
A: dead-code
Dead code elimination and --save-metas.
A: errors
Reporting of error and warning messages.
A: highlighting
Highlighting during interaction & literate compilation
A: imports
Handling of imports and interface file de/serialization.
A: infra
Iinfrastructure (e.g. CI, developer documentation, the build system, or the repository itself)
A: instance
Instance declarations, arguments, and resolution
A: lhs
LHS checking, coverage checking, and clause compilation
A: modules
Declaration and instantiation of parametrised modules.
A: parallel
Parallel typechecking.
A: positivity
Positivity checking
A: printing
Pretty-printing, display forms, and the wording of diagnostic messages
A: records
Record declarations, record expressions and copattern matching
A: scoping
Scope checking (ConcreteToAbstract)
A: termination
Termination checking
0 - type
bug
 Issues describing an incorrect behaviour in the project, typos in the documentation, etc.
0 - type
discussion
 An issue raised to gather opinions on a proposed change, or a suggested language change.
0 - type
question
 An issue raised to ask a question.
9 - status
duplicate
 This issue or pull request already exists.
9 - status
info needed
 More information is needed from the submitter to decide how to proceed with the issue report.
9 - status
invalid
 The issue report or pull request does not describe an actual bug, or does otherwise does not meet the contributing guidelines.
good first issue
Interested in contributing? Get started here.
upstream
Related to an upstream repository, already reported there
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
2 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
1lab/mikan!55
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "ncf/mikan:erase-erasure"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?