Email Gateway (Aug 22 2022 at 20:04): Email Gateway (Aug 22 2022 at 20:04):From: "Zelmat, Oliver Amine" <oliver.amine.zelmat@rwth-aachen.de>
Hello,
I have some problems with the domain keyword and quickcheck. I have defined a domain with
domain lnat = lnsuc (lazy lnpred::lnat)
How can I setup quickcheck do find a counter example for this lemma
lemma "lnsuc⋅⊥ = ⊥"
quickcheck
I get the error message
Type unification failed: No type arity lnat :: term_of
Type error in application: incompatible operand type
Operator: term_of_class.term_of :: ??'a ⇒ term
Operand: lnsuc⋅⊥ :: lnat
Is there a possibility to get code equations of the constructor lnsuc?
Thanks for any insights
Oliver Zelmat
Email Gateway (Aug 22 2022 at 20:04):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think quickcheck is set up to deal with HOLCF domains at all. The
presence of nontermination makes it difficult.
Tobias
smime.p7s
Last updated: Apr 23 2024 at 08:19 UTC