I am a newbie in Isabelle/hol and I have this record declaration:
record ('v,'w) fca = object_set :: "'v set" attribute_set :: "'w set" inc_set :: "('v×'w) set"
and I want to instantiate to obtain a concrete record like:
definition Concrete_fca :: fca where "pt1 ≡ (| object_set ={''a'',''b'',''c''}, attribute_set = {1::nat,2,3},inc_set = {(''a'', 1),(''a'',3)} |)"
But, I am getting an error: Bad number of arguments for type constructor: tuto2.fca
NB: tuto2 is the name of my theory and fca is the name of the record Please can someone help me resolve this issue. Thanks
I searched online for the same type of errors.
There are two problems with your definition. First, fca is a type constructor, not a type, so you must apply it to some type arguments to get a type (this is what the error tells you). In your case this is (string, nat).
The other problem is that you want to define Concrete_fca but then give an equation for pt1. Giving the same name in both places gives you something like this:
definition Concrete_fca :: "(string, nat) fca" where
"Concrete_fca ≡ (| object_set ={''a'',''b'',''c''}, attribute_set = {1::nat,2,3},inc_set = {(''a'', 1),(''a'',3)} |)"