Skip to content

Harpoon: Uncaught exception when attempting to split/invert something #257

@chutasano

Description

@chutasano

I think? this is an error. I'm trying to split/invert something in my computation context, and I get the following error:

Theorem: pres_step
intros <- split fwd (case beta_fwd) <- split x1 (case tp_jdg_par)
Meta-context:
  g : ctx
  X : ( |- tp)
  X1 : (g |- name)
  X2 : (g, x : name |- proc)
  X4 : ( |- tp) (not in scope)
  X7 : ( |- dual X X4)
  X8 : (g, x : name, y : hyp x X[] |- tp_jdg (fwd (X1[..]) x))
  X9 : (g, x : name, z : hyp x X4[] |- tp_jdg (X2[.., x]))
  X10 : (g |- linear (\x14. fwd (X1[..]) x14))
  X11 : (g |- linear (\x14. X2))
Computational context:
  x : [g |- tp_jdg (pcomp X[] (\x. ppar (fwd (X1[..]) x) X2))]
  x1 : [g |- step (pcomp X[] (\x. ppar (fwd (X1[..]) x) X2)) (X2[.., X1])]
  fwd : [g, b : block (x : name, h : hyp x X[]) |- tp_jdg (fwd (X1[..]) b.1)]
       
--------------------------------------------------------------------------------
[g |- tp_jdg (X2[.., X1])]
       
> split fwd
Uncaught exception.
Please report this as a bug.
Internal error. (State may be undefined.)
Failure("Found Clo - should not happen")

Metadata

Metadata

Assignees

No one assigned

    Labels

    A | coreaffecting the typecheckerA | harpoonaffecting the Harpoon interactive proverB | bugunexpected or incorrect behaviour

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions