Stream: General

Topic: Groups_Big type problem

Gergely Buday (Sep 13 2023 at 10:26):

I have a minimal non-working example for a type problem:

theory Groups_Big_Type_Problem

imports Main

begin

context comm_monoid_set

begin

value "F"

end

end

On this, Isabelle gives a type constraint error:

Sort constraint equal inconsistent with default type for type variable "'a"

How can I make Isabelle show the type at F's definition at HOL.Groups_Big?

definition F :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'a"
  where eq_fold: "F g A = Finite_Set.fold (f ∘ g) ❙1 A"

Mathias Fleury (Sep 13 2023 at 15:42):

term F
(*
"F"
  :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'a"
*)

Mathias Fleury (Sep 13 2023 at 15:42):

Unlike value, term does not involve the code generator…

Gergely Buday (Sep 14 2023 at 12:40):

@Mathias Fleury how code generation comes to the picture here?

Mathias Fleury (Sep 14 2023 at 12:59):

value does code generation

Last updated: May 02 2024 at 08:19 UTC