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

rename Set to Type #112

Merged
amyliao merged 2 commits from ncf/mikan:set-to-type into main 2026年05月27日 18:09:46 +02:00
Owner
Copy link

Closes #37.

Remaining work:

  • Emit a warning when Set(ω)(i) is used and not in scope.
  • Figure out why some test outputs now have leading blank lines (e.g. test/Succeed/TooManyPolarities.warn): the leading blank lines were actually added by github.com/agda/agda@b9529c88e7 but the golden outputs were not changed because whitespace is normalised.
Closes https://codeberg.org/1lab/mikan/issues/37. Remaining work: - [x] Emit a warning when `Set(ω)(i)` is used and not in scope. - [x] Figure out why some test outputs now have leading blank lines (e.g. `test/Succeed/TooManyPolarities.warn`): the leading blank lines were actually added by https://github.com/agda/agda/commit/b9529c88e754ad2c2bfa21c1dc77d63587eef3ca but the golden outputs were not changed because whitespace is normalised.
@ -135,1 +132,4 @@
dataSort:Type
dataPattern:Type
dataClause:Type
Type=Term
Owner
Copy link

that's gonna cause problems

that's gonna cause problems
ncf marked this conversation as resolved
ncf force-pushed set-to-type from f2cbce4062
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 41c2c099b4
Some checks failed
ci/woodpecker/pr/test Pipeline failed
2026年05月19日 20:02:14 +02:00 Compare
ncf force-pushed set-to-type from 41c2c099b4
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 372e4ec92d
Some checks failed
ci/woodpecker/pr/test Pipeline failed
2026年05月19日 20:44:59 +02:00 Compare
ncf force-pushed set-to-type from 372e4ec92d
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 21894875af
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月19日 22:09:36 +02:00 Compare
ncf force-pushed set-to-type from 21894875af
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to b703a4b6c7
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月19日 23:10:27 +02:00 Compare
ncf force-pushed set-to-type from b703a4b6c7
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to f908d7c928
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月20日 13:32:50 +02:00 Compare
ncf force-pushed set-to-type from f908d7c928
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to c80aae5735 2026年05月20日 14:15:45 +02:00 Compare
Author
Owner
Copy link

1Lab patch: https://gist.github.com/ncfavier/42254bed6c8ef4a2903fc7786dfa5c5b

1Lab patch: https://gist.github.com/ncfavier/42254bed6c8ef4a2903fc7786dfa5c5b
ncf changed title from (削除) WIP: rename Set to Type (削除ここまで) to rename Set to Type 2026年05月20日 14:16:54 +02:00
ncf force-pushed set-to-type from c80aae5735 to a7635d1560
Some checks failed
ci/woodpecker/pr/test Pipeline failed
2026年05月21日 16:25:57 +02:00 Compare
ncf force-pushed set-to-type from a7635d1560
Some checks failed
ci/woodpecker/pr/test Pipeline failed
to 51d50a48ab
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月21日 17:11:21 +02:00 Compare
ncf force-pushed set-to-type from 51d50a48ab
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to dc2cca99d2
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
2026年05月21日 22:41:26 +02:00 Compare
ncf force-pushed set-to-type from dc2cca99d2
All checks were successful
ci/woodpecker/pr/test Pipeline was successful
to 6b39d3dfda
All checks were successful
ci/woodpecker/push/main Pipeline was successful
2026年05月27日 16:57:26 +02:00 Compare
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!112
Reference in a new issue
1lab/mikan
No description provided.
Delete branch "ncf/mikan:set-to-type"

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?