Email Gateway (Aug 18 2022 at 11:24): Email Gateway (Aug 18 2022 at 11:24):From: Rajesh Karunamurthy <rajesh.karuna@yahoo.com>
Hi,
I am a new Isabelle user. I have some questions regarding the usage of string types with records.
Can I define something like this as a record definition
record class =
className :: string
classType :: string
or
should the same be defined using 'char' data type. If the above
definition is allowed and correct then how can this be 'concretely'
defined. Basically, how can I define a constant of type 'class'? Can
someone please provide some pointers for any examples that uses string
types in records?
Thanks for the help,
Rajesh
____________________________________________________________________________________
Looking for last minute shopping deals?
Find them fast with Yahoo! Search. http://tools.search.yahoo.com/newsearch/category.php?category=shopping
Email Gateway (Aug 18 2022 at 11:24):From: Makarius <makarius@sketis.net>
Yes, here is an example:
record "class" =
class_name :: string
class_type :: string
definition "my_class = (| class_name = ''foo'', class_type = ''bar'' |)"
Makarius
Last updated: May 03 2024 at 04:19 UTC