Skip to content

GitLab

Closed
Created by Ralf Jung@jungOwner

iDestruct on non-existing name yields "no matching clause for match"

Title says it all. Goal state:

============================
  ​"Hincl" : type_incl ty1 ty2
  "Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
  "Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
  "Hsincl" : ∀ (κ0 : lft) (tid0 : thread_id) (l0 : loc),
             ty_shr ty1 κ0 tid0 l0 -∗ ty_shr ty2 κ0 tid0 l0
  --------------------------------------□
  ​"Hshr" : ty_shr (rc ty1) κ tid l
  --------------------------------------∗
  ty_shr (rc ty2) κ tid l

Tactic: iDestruct "Hst" as (??) "H". Error: Error: No matching clauses for match.