Commit a2eb60e7 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix inconsistency of map.MapPermut detected by Benedikt Huber.

This reverts part of commit b45604c2.
parent b63a3d60
...@@ -85,7 +85,6 @@ theory MapPermut ...@@ -85,7 +85,6 @@ theory MapPermut
use import int.Int use import int.Int
use export Map use export Map
use import MapEq
predicate exchange (a1 a2 : map int 'a) (i j : int) = predicate exchange (a1 a2 : map int 'a) (i j : int) =
a1[i] = a2[j] /\ a2[i] = a1[j] /\ a1[i] = a2[j] /\ a2[i] = a1[j] /\
...@@ -97,8 +96,7 @@ theory MapPermut ...@@ -97,8 +96,7 @@ theory MapPermut
inductive permut_sub (map int 'a) (map int 'a) int int = inductive permut_sub (map int 'a) (map int 'a) int int =
| permut_refl : | permut_refl :
forall a1 a2 : map int 'a. forall l u : int. forall a : map int 'a. forall l u : int. permut_sub a a l u
map_eq_sub a1 a2 l u -> permut_sub a1 a2 l u
| permut_sym : | permut_sym :
forall a1 a2 : map int 'a. forall l u : int. forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u permut_sub a1 a2 l u -> permut_sub a2 a1 l u
......
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