Questions tagged [locales]

Locales are Isabelle’s approach for dealing with parametric theories. They have been designed as a module system for a theorem prover that can adequately represent the complex inter-dependencies between structures found in abstract algebra, but have proven fruitful also in other applications — for example, software verification. (from Tutorial to Locales and Locale Interpretation)

Filter by
Sorted by
Tagged with
15 votes
0 answers

Code generation from Locales and Sublocales in Isabelle

Problem Description I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in ...
Wno-all's user avatar
  • 1,098
12 votes
1 answer

What are "locales" in Isabelle?

How does it compare to dependent records in Agda/Lean/etc.? I heard that locales in Isabelle are used to model algebraic structures in a talk, bu. Isn't this a kind of dependent type in some sense? Is ...
ice1000's user avatar
  • 5,974