Visitar URL original
Erase exports by dancewithheart · Pull Request #19 · wasabi315/aegle · GitHub
Skip to content

Erase exports - #19

Merged
wasabi315 merged 9 commits into
wasabi315:mainfrom
dancewithheart:erase-exports
Oct 24, 2026
Merged

Erase exports#19
wasabi315 merged 9 commits into
wasabi315:mainfrom
dancewithheart:erase-exports

Conversation

@dancewithheart

@dancewithheart dancewithheart commented Oct 19, 2026

Copy link
Copy Markdown
Contributor

Partially address #12

Add predicate:

isIndexableDefinition :: Definition -> Transl Bool
isIndexableDefinition def = case def.theDef of
  DataOrRecSigDefn {} -> pure False
  GeneralizableVar {} -> pure False
  PrimitiveSortDefn {} -> pure False
  _ -> not <$> isErasable def.defType

and use it in translateScope and translateDefinition

Tested with:

stack test aegle-index

@wasabi315

wasabi315 commented Oct 21, 2026

Copy link
Copy Markdown
Owner

Thank you very much for your PR! I have several things I would like you to address. Could you check my review comments?

wasabi315
wasabi315 reviewed Oct 21, 2026
View reviewed changes
Comment thread aegle-index/test/Main.hs Resolved
Comment thread aegle-index/test/Main.hs Resolved
Comment thread aegle-index/test/Main.hs Resolved
Comment thread aegle-index/test/Main.hs Resolved
Comment thread aegle-index/src/Aegle/Index/Translate/Definition.hs Resolved
Comment thread aegle-index/src/Aegle/Index/Translate/Scope.hs Resolved
dancewithheart and others added 6 commits October 21, 2026 16:13
@dancewithheart @wasabi315
Update aegle-index/src/Aegle/Index/Translate/Definition.hs
a02bec0 
Co-authored-by: Satoshi Takimoto <wasabi.nvim.st@gmail.com>
@dancewithheart @wasabi315
Update aegle-index/test/Main.hs
7006013 
Co-authored-by: Satoshi Takimoto <wasabi.nvim.st@gmail.com>
@dancewithheart @wasabi315
Update aegle-index/test/Main.hs
e323988 
Co-authored-by: Satoshi Takimoto <wasabi.nvim.st@gmail.com>
@dancewithheart @wasabi315
Update aegle-index/test/Main.hs
7fbd1b5 
Co-authored-by: Satoshi Takimoto <wasabi.nvim.st@gmail.com>
@dancewithheart
review use ifNotM in translateScope
b339ac8
@dancewithheart
review replace property Hedgehog with example test sining Testy
cfa613f
@dancewithheart

dancewithheart commented Oct 22, 2026

Copy link
Copy Markdown
Contributor Author

Thank you for your time and careful review 🙇 I applied your remarks. Can you re-review?

wasabi315
wasabi315 approved these changes Oct 24, 2026
View reviewed changes

@wasabi315 wasabi315 left a comment

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@wasabi315

wasabi315 commented Oct 24, 2026

Copy link
Copy Markdown
Owner

Thank you for your contribution!

@wasabi315
wasabi315 merged commit 037e78c into wasabi315:main Oct 24, 2026
@dancewithheart

dancewithheart commented Oct 24, 2026

Copy link
Copy Markdown
Contributor Author

It was fun!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@wasabi315 wasabi315 wasabi315 approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@dancewithheart @wasabi315