Stream: Beginner Questions

Topic: Traits -> Isabelle


view this post on Zulip Max Nowak (Aug 10 2021 at 19:19):

I want to model the following Rust code, but in Isabelle:

trait Ballot<A> {
  fn on_options(&self) -> Set<A>;
  fn prefers(&self, a: A, b: A) -> bool;
  // assumes reflexivity, etc
}

struct Profile<A, T: Ballot<A>> {
  ballots: List<T>,
}

I tried to do it with typeclasses, but I think I'm on the wrong path:

class ballot =
  fixes on_options :: "'a set"
  fixes prefers :: "'a ⇒ 'a ⇒ bool"
  assumes (* ... *)

Help?

view this post on Zulip Mathias Fleury (Aug 13 2021 at 08:00):

It depends what you are trying to achieve:

view this post on Zulip Max Nowak (Aug 13 2021 at 10:26):

Yeah it's intended for a conrete problem, not an arbitrary Rust program. Thank you!


Last updated: Aug 15 2022 at 04:16 UTC