Isabelle Syntax

Moderator: Modellierungspraktikum

jon as
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 23. Nov 2014 23:14

Isabelle Syntax

Beitrag von jon as » 5. Nov 2015 18:17

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

jon as
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 23. Nov 2014 23:14

Re: Isabelle Syntax

Beitrag von jon as » 9. Nov 2015 08:58

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

Antworten

Zurück zu „Modellierungspraktikum“