Theory Type_Classes

section ‹Type Classes›

theory Type_Classes
imports Main
begin

text ‹Overloaded functions:›

class is_empty = 
  fixes is_empty :: "'a ⇒ bool"

class invar =
  fixes invar :: "'a ⇒ bool"

class size_new =
  fixes size_new :: "'a ⇒ nat"

class step =
  fixes step :: "'a ⇒ 'a"

class remaining_steps =
  fixes remaining_steps :: "'a ⇒ nat"

end