20881.why 490 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
theory Bug
26
    use map.Map
MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31 32 33 34 35 36 37

    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