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.

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

🆔 Introduce !def and make def non-shadowing #319

Closed
favonia opened this issue Mar 12, 2022 · 1 comment · Fixed by #340
Closed

🆔 Introduce !def and make def non-shadowing #319

favonia opened this issue Mar 12, 2022 · 1 comment · Fixed by #340
Labels
papercut Minor annoyances that would be nice to fix

Comments

@favonia
Copy link
Collaborator

favonia commented Mar 12, 2022

A spin-off proposal from #312.

@favonia favonia added the papercut Minor annoyances that would be nice to fix label Mar 12, 2022
@favonia
Copy link
Collaborator Author

favonia commented Mar 24, 2022

The non-shadowing def is actually useful. It detected this suspicious code:

cooltt/test/isos.cooltt

Lines 83 to 101 in 2fc8cfa

def iso/lhs (A B C : type) (I : iso A B) : iso {A → C} {B → C} :=
let f := fst I in
let g := fst {snd I} in
let α := fst {snd {snd I}} in
let β := snd {snd {snd I}} in
[ac b => ac {g b},
[bc a => bc {f a},
[bc i b => bc {α b i},
ac i a => ac {β a i}]]]
def iso/lhs (A B C : type) (I : iso A B) : iso {C → A} {C → B} :=
let f := fst I in
let g := fst {snd I} in
let α := fst {snd {snd I}} in
let β := snd {snd {snd I}} in
[ca c => f {ca c},
[cb c => g {cb c},
[cb i c => α {cb c} i,
ca i c => β {ca c} i]]]

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
papercut Minor annoyances that would be nice to fix
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant