Bounded quantification
g = %L %a <= { one : Int }. %l x: %a. (x.one)
g : \A %a <= { one : int }. %a -> Int
g' = %L %b . %L %a <= { one : %b }. %l x: %a. (x.one)
g' : \A %b . \A %a <= { one : %b }. %a -> %b
move = %L %a <= Point. %l p:%a. %l d : Int .(p.x := p.x + d); p
move : \A %a <= Point. %a -> Int -> %a
Application
g' [ Int ][ { one:Int, two : Bool }]({ one = 3, two = true }) = 3
move [{ x : Int, y : Int }]( { x = 0, y = 0 } )(1) = { x = 1, y = 0 }
slide
:
Bounded quantification -- examples
