RedPRL/cooltt

🆔 Introduce `!def` and make `def` non-shadowing

Closed this issue · 1 comments

A spin-off proposal from #312.

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]]]