equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>Example of lifting definitions with contravariant or co/contravariant type variables\<close> |
5 section \<open>Example of lifting definitions with contravariant or co/contravariant type variables\<close> |
6 |
6 |
7 |
7 |
8 theory Lift_Fun |
8 theory Lift_Fun |
9 imports Main "~~/src/HOL/Library/Quotient_Syntax" |
9 imports Main "HOL-Library.Quotient_Syntax" |
10 begin |
10 begin |
11 |
11 |
12 text \<open>This file is meant as a test case. |
12 text \<open>This file is meant as a test case. |
13 It contains examples of lifting definitions with quotients that have contravariant |
13 It contains examples of lifting definitions with quotients that have contravariant |
14 type variables or type variables which are covariant and contravariant in the same time.\<close> |
14 type variables or type variables which are covariant and contravariant in the same time.\<close> |