au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

multilines in table file breaks CorresSetup #402

Closed amblafont closed 3 years ago

amblafont commented 3 years ago
main : {  field1 : U32 } -> {  field1 : U32 }
main x = x

The CorresSetup generated theory file fails : reading table raises the error "expected " :=: ", because the generated table file is multiline:

TRecord [
  (
    ''field1'',
    (
      TPrim (Num U32),
      Present
    )
  )
] (Boxed Writable undefined) :=: t1
amblafont commented 3 years ago

solved by some recent commit