Commit 1f163b68 authored by MARCHE Claude's avatar MARCHE Claude

BTS 13849

parent 8c69db4c
(* BTS 13849 *)
theory T
type t = T
type x 'a 'b =
| X t 'a
| Y t 'b
type a = A0 | A1
type b = B
function b1 : x a b = (X T A0)
function b2 : x a b = (X T A1)
goal x : b1 = b2
(* Theorem x1 : ((X(T, A0):(x a b)) = (X(T, A1):(x a b))).*)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="13849/why3session.xml">
<prover
id="0"
name="Coq"
version="8.3pl3"/>
<file
name="../13849.why"
verified="false"
expanded="true">
<theory
name="T"
locfile="13849/../13849.why"
loclnum="4" loccnumb="7" loccnume="8"
verified="false"
expanded="true">
<goal
name="x"
locfile="13849/../13849.why"
loclnum="19" loccnumb="6" loccnume="7"
sum="15dd0a14b365705789dc555517dcc6cd"
proved="false"
expanded="true"
shape="ainfix =ab1ab2">
<proof
prover="0"
timelimit="5"
edited="13849_T_x_1.v"
obsolete="true"
archived="false"><unedited/>
</proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment