adjust definition of isAction

cedar-lean/Cedar/Spec/Value.lean

@@ -47,9 +47,6 @@ structure EntityUID where
   ty : EntityType
   eid : String
 
-def EntityUID.isAction (uid : EntityUID) : Bool :=
-  uid.ty.id == "Action"
-
 inductive Prim where
   | bool (b : Bool)
   | int (i : Int)

cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean

@@ -95,7 +95,7 @@ action store, and the ancestor relationships in the entity store are consistent
 with the descendants information in the action store.
 -/
 def InstanceOfActionStore (entities : Entities) (as: ActionStore) : Prop :=
-  ∀ uid data, entities.find? uid = some data → uid.isAction →
+  ∀ uid data, entities.find? uid = some data → isAction uid as →
     ∀ ancestor, ancestor ∈ data.ancestors →
       ∃ descendants, as.find? ancestor = some descendants ∧ uid ∈ descendants
 

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -127,9 +127,12 @@ def entityUIDs? : Expr → Option (List EntityUID)
   | .set xs => xs.mapM entityUID?
   | _       => .none
 
+def isAction (uid : EntityUID) (acts: ActionStore) : Bool :=
+  acts.contains uid
+
 def actionUID? (x : Expr) (acts: ActionStore) : Option EntityUID := do
   let uid ← entityUID? x
-  if acts.contains uid then .some uid else .none
+  if isAction uid acts then .some uid else .none
 
 -- x₁ in x₂ where x₁ has type ety₁ and x₂ has type ety₂
 def typeOfInₑ (ety₁ ety₂ : EntityType) (x₁ x₂ : Expr) (env : Environment) : ResultType :=
@@ -284,4 +287,4 @@ def typeOf (x : Expr) (c : Capabilities) (env : Environment) : ResultType :=
     let tys ← xs.mapM₁ (λ ⟨x₁, _⟩ => justType (typeOf x₁ c env))
     typeOfCall xfn tys xs
 
-end Cedar.Validation
+end Cedar.Validation