Stream: Beginner Questions

Topic: Traits -> Isabelle

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?

Mathias Fleury (Aug 13 2021 at 08:00):

It depends what you are trying to achieve:

• if you intend to do that for a single problem, then I would use locales instead of classes.
• if you are trying to do that for arbitrary Rust programs, then locales will not work (or you need to generate them programatically and I don't believe that will scale) .

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: Apr 25 2024 at 20:15 UTC