Howdy! I'm playing around with formalizing generalized sudoku in Coq. "Generalized" in the sense that the game is parameterized by two `nat`

values describing grid size. So I'm going to have a big chunk of (interdependent, type-heavy) code with those parameters. I'm going to want to instantiate that chunk of code by providing the parameters once, and receiving an object representing the specialized sudoku library.

Would you recommend using type classes? Modules? Sections? Something else? If you know of a relevant code example I could look at I would love that.

What do you mean by code? It is just definitions and lemmas, or Ltac, Notations, ...

Minimally, definitions and lemmas; ideally, all of the above.

Functors can abstract almost anything over a module, that would be the most "generic" abstraction you have. Type Classes and co are nice because instances are found automatically, while you have to manually apply functors. But for your use case this does not seem to be a big issue, I guess.

@Carl Patenaude-Poulin are you aware of this? https://github.com/coq-contribs/sudoku

most people use a combination of (1) sections + ltac + notations and (2) one of: modules, type classes, canonical structures

Nice, I'll try functors. Much appreciated.

@Karl Palmskog I've heard of the sudoku library, I plan on looking at it once I get stuck

Last updated: Jun 15 2024 at 05:01 UTC