Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
4dcb456d
Commit
4dcb456d
authored
Feb 17, 2015
by
Guillaume Melquiond
Browse files
Make the bench compatible with the changes to inductive types in Coq 8.5.
parent
493c3127
Changes
1
Hide whitespace changes
Inline
Side-by-side
bench/coq-tactic/test.v
View file @
4dcb456d
...
...
@@ -254,15 +254,15 @@ Qed.
(
*
Polymorphic
,
Mutually
inductive
types
*
)
Inductive
ptree
(
a
:
Set
)
:
Set
:=
|
PLeaf
:
ptree
a
|
PNode
:
a
->
pforest
a
->
ptree
a
Inductive
ptree
{
a
:
Set
}
:
Set
:=
|
PLeaf
:
ptree
|
PNode
:
a
->
pforest
->
ptree
with
pforest
(
a
:
Set
)
:
Set
:=
|
PNil
:
pforest
a
|
PCons
:
ptree
a
->
pforest
a
->
pforest
a
.
with
pforest
{
a
:
Set
}
:
Set
:=
|
PNil
:
pforest
|
PCons
:
ptree
->
pforest
->
pforest
.
Goal
forall
x
:
ptree
Z
,
x
=
x
.
Goal
forall
x
:
@
ptree
Z
,
x
=
x
.
ae
.
Qed
.
...
...
@@ -277,18 +277,18 @@ Goal bb=0.
ae
.
Qed
.
Fixpoint
ptree_size
(
a
:
Set
)
(
t
:
ptree
a
)
:
Z
:=
match
t
with
Fixpoint
ptree_size
{
a
:
Set
}
(
t
:
@
ptree
a
)
:
Z
:=
match
t
with
|
PLeaf
=>
0
|
PNode
_
f
=>
1
+
pforest_size
_
f
end
with
pforest_size
(
a
:
Set
)
(
f
:
pforest
a
)
:
Z
:=
match
f
with
|
PNode
_
f
=>
1
+
pforest_size
f
end
with
pforest_size
{
a
:
Set
}
(
f
:
@
pforest
a
)
:
Z
:=
match
f
with
|
PNil
=>
0
|
PCons
t
f
=>
ptree_size
_
t
+
pforest_size
_
f
end
.
|
PCons
t
f
=>
ptree_size
t
+
pforest_size
f
end
.
Goal
ptree_size
_
(
@
PLeaf
Z
)
=
0.
Goal
ptree_size
(
@
PLeaf
Z
)
=
0.
ae
.
Qed
.
Goal
forall
(
a
:
Set
),
ptree_size
a
(
PLeaf
a
)
=
0.
Goal
forall
(
a
:
Set
),
ptree_size
(
@
PLeaf
a
)
=
0.
intros
.
ae
.
Qed
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment