Seite 1 von 1

Isabelle Syntax

Verfasst: 5. Nov 2015 18:17
von jon as
Hey,

There are few Tutorials about Isabell. There are a few pdf's in Isabelle itself, but a google search to specific problems is quite impossible.

I tryd for example to create a datatype someB (which is equivalent too bool). I create a variable ex1 of type someB. I just want to assigne the value True to that variable. The following code does not work. Does anyone have an idea why? I am probably doing something fundamentally wrong.

datatype someB = "bool"

definition
ex1 :: someB where "ex1 ≡ True"


Fehlermeldung:
Type unification failed: Clash of types "bool" and "someB"

Type error in application: incompatible operand type

Operator: op ≡ ex1 :: someB ⇒ prop
Operand: True :: bool


Thank you
Jonas

Re: Isabelle Syntax

Verfasst: 9. Nov 2015 08:58
von jon as
Hi,
das ließt hier wahrscheinlich eh niemand. Egal. Ich habe vielleicht Abhilfe gefunden. In dem Isar-ref.pdf gibt es railroad diagrams welche nicht nur cool aussehen sondern vielleicht auch benutztbar sind um die Sprache zu lernen.

so long guys,
Jonas