20881.why 497 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24


theory OK

type t 'a = A | B (t 'a)


goal g : forall x: t 'a. A <> B x

end


theory Bug1

type t 'a = A int

function f (t 'a) : 'a

goal g : let p = (A 0: t int) in
         let q = (A 1: t int) in
         f p = f q

end

MARCHE Claude's avatar
MARCHE Claude committed
25 26 27 28 29 30 31 32 33 34 35 36 37
theory Bug
    use import map.Map

    type t
    type p 'a = PTR t

    function load (p 'a) :'a

    goal bug: forall i.
        let p = ((PTR i):(p (map t t))) in
        let q = ((PTR i):(p t)) in
    (load p)[i] = (load q)
end