Add Generator for Cedar Terms

[ngernest]

This PR adds a Lean formalization of a subset of Cedar to the list of examples in the Test directory.

Relevant files:

• Cedar.lean: Lean formalization of a subset of the Cedar policy language (OOPSLA '24), adapted from Mike Hicks's Coq formalization
• CedarCheckerGenerators.lean: Snapshot tests for derived checkers & generators for Cedar terms / types / schemas
• CedarWellTypedTermGenerator.lean: Example generator for well-typed Cedar expressions

Note: Chamelean can only handle 23 out of the 41 typing rules -- if we give it all 41 typing rules, it takes > 5 minutes to derive a generator.

The remaining 18 rules which Chamelean takes too long to handle are rules involving multiple constraints expressed via auxiliary relations, e.g.:

-- Chamelean has trouble handling the `TContainsAll` constructor since it involves multiple constraints
-- expressed via auxiliary inductive relations, e.g. `DefinedEntities`, `WfCedarType`, `SubType`
inductive HasType : PathSet → Environment → (CedarExpr × PathSet) → CedarType → Prop where
| TContainsAll : ∀ a x1 x2 V E1 E2 ets acts R ns T1 T2 T,
    V = (Environment.MkEnvironment (Schema.MkSchema ets acts) R) →
    DefinedEntities ets ns →
    WfCedarType ns T →
    SubType T1 T → SubType T2 T →
    HasType a V (E1, x1) (CedarType.setType T1) →
    HasType a V (E2, x2) (CedarType.setType T2) →
    HasType a V ((CedarExpr.binaryApp BinaryOp.containsAll E1 E2), PathSet.somepaths []) (CedarType.boolType BoolType.anyBool)
| ...

Since some of the typing rules have been commented out, the generator for Cedar terms doesn't produce well-typed terms at the moment (see the comments in CedarWellTypedTermGenerator.lean for details).