search

spechub / Hets

The Heterogeneous Tool Set
http://hets.eu
GNU General Public License v2.0
57 stars 19 forks source link

Translation to Isabelle: let cases and classes #131

Open sternk opened 10 years ago

sternk commented 10 years ago

Reported by maeder and assigned to maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/131

special let cases and classes still need to be translated to Isabelle

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/131#comment:4

implemented let expressions where partial results are assigned to a single variable

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/131#comment:6

Several theories in HasCASL/Metatheory/ (Functor and Monad) fail with

funType: no higher kinds

Furthermore:

could not translate to Isabelle file: HasCASL/Metatheory/Ord_Ord.thy
*** Error, not a function type
sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/131#comment:7

and hets -o thy HasCASL/EuclideanSpaces.het fails with transOpId

sternk commented 10 years ago

Comment by maeder Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/131#comment:8

the transOpId failure is fixed with #413