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

[#197] Dependent RepoInfo keys example #243

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

[#197] Dependent RepoInfo keys example #243

wants to merge 1 commit into from

Commits on Dec 15, 2022

  1. [#197] Dependent RepoInfo keys example 

    Problem: During the implementation of issue #197, we though about how we
could customize the way filepaths are searched within the repository data
in an efficient way, depending on if filepaths are case-insensitive or not.

Solution: We implemented a GADT with its polymorphic parameter, corresponding
to Map keys, hidden under an existentially quantified type. Although we end up
not requiring this, we separate the essence of the idea to a commit in a
separate branch, so it can be reviewed in the future.
    @aeqz
    aeqz committed Dec 15, 2022
    Configuration menu
    Copy the full SHA
    90abffe View commit details
    Browse the repository at this point in the history