Open LorenNuyts opened 4 years ago
The OCaml output file contains errors the way it is generated at the moment. The code for generating the OCaml output should be updated such that it generates correct OCaml code and is up-to-date with the current Haskell output.
For example `namespace TermVar: Term
sort Term inh ctx TermVar | Var (x@ctx) | Lam (t: Term) [x: TermVar] t.ctx = lhs.ctx, x | App (t1: Term) (t2: Term) | Prod (t1: Term) (t2: Term) | Let (p: Pat) (t1: Term) (t2: Term) p.ictx = lhs.ctx t2.ctx = p.sctx
sort Pat inh ictx TermVar syn sctx TermVar | PVar [x: TermVar] lhs.sctx = lhs.ictx, x | PProd (p1: Pat) (p2: Pat) p1.ictx = lhs.ictx p2.ictx = p1.sctx lhs.sctx = p2.sctx ` results in a syntax error in the output file on line 49, characters 81-82.
The OCaml output file contains errors the way it is generated at the moment. The code for generating the OCaml output should be updated such that it generates correct OCaml code and is up-to-date with the current Haskell output.
For example `namespace TermVar: Term
sort Term inh ctx TermVar | Var (x@ctx) | Lam (t: Term) [x: TermVar] t.ctx = lhs.ctx, x | App (t1: Term) (t2: Term) | Prod (t1: Term) (t2: Term) | Let (p: Pat) (t1: Term) (t2: Term) p.ictx = lhs.ctx t2.ctx = p.sctx
sort Pat inh ictx TermVar syn sctx TermVar | PVar [x: TermVar] lhs.sctx = lhs.ictx, x | PProd (p1: Pat) (p2: Pat) p1.ictx = lhs.ictx p2.ictx = p1.sctx lhs.sctx = p2.sctx ` results in a syntax error in the output file on line 49, characters 81-82.