search

Orbis-Tertius / osl

Apache License 2.0
2 stars 2 forks source link

Name shadowing bug #6

Closed morganthomas closed 2 years ago

morganthomas commented 2 years ago

Steps to reproduce:

Compile foo and bar defined in this spec:

def c : N -> N := \x : N => x.

def foo : N -> Prop
  := \x : N => c(x) = x.

def bar : N -> Prop
  := \c : N => foo(c).

Expected result:

Both compile to the same result.

Actual result:

bar does not compile.

Explanation:

c is shadowed. bar compiles upon alpha conversion.

morganthomas commented 2 years ago

Fixed.