Isabelle/HOL记录类型构造器参数数量错误求助

错误原因 #

你的fca记录是带两个类型参数的多态类型（'v对应对象类型，'w对应属性类型），定义具体实例时必须明确指定这两个参数，仅写fca会导致类型构造器参数数量不匹配，触发Bad number of arguments错误。此外你定义语句中存在变量名不一致的问题（定义名Concrete_fca和右边的pt1不匹配）。

修正后的代码 #

record ('v,'w) fca =
  object_set :: "'v set"
  attribute_set :: "'w set"
  inc_set :: "('v×'w) set"

-- 明确指定类型参数：对象为string，属性为nat；同时统一变量名
definition Concrete_fca :: "fca string nat" where
  "Concrete_fca ≡ (| object_set = {''a'', ''b'', ''c''},
                     attribute_set = {1::nat, 2, 3},
                     inc_set = {(''a'', 1), (''a'', 3)} |)"

验证方法 #

可以用value命令查看实例化后的记录值：

value "Concrete_fca"

内容的提问来源于stack exchange，提问作者Jceric