CODEWITHSUNDEEP
isabelle
alagris
alagris

Reputation: 2206

Isabelle definitions with subscripts

I the Tutorial on (Co)datatype Definitions https://isabelle.in.tum.de/dist/Isabelle2022/doc/datatypes.pdf in Introduction I see the definition

datatype 'a tree_fs = Node_fs (lbl_fs:'a) (sub_fs: “'a tree_fs fset ”)

where _fs are written in subscript. Then they are used with different subscripts later on, suggesting that those subscripts are not merely a fancy design but can actually be "instantiated" in some sense. Where can I find more information about it and how can I use such subscripts?

Upvotes: 0

Views: 127

Answers (1)

Javier Díaz
Javier Díaz

Reputation: 1081

Those subscripts can be instantiated using the predefined symbol \<^sub>, which you can insert in Isabelle/JEdit by typing \sub (literally) and choosing the down arrow icon that shows up in the dropdown list. In the specific example you refer to, you need to include a subscript for each letter f and s individually, that is, \<^sub>f\<^sub>s.

You can read more about this in The Isabelle/Isar Reference Manual, Appendix A "Predefined Isabelle symbols".

Upvotes: 1

Related Questions