diff --git a/cedar-lean/CedarProto/Expr.lean b/cedar-lean/CedarProto/Expr.lean
index f03d080f9..47d0c0c1a 100644
--- a/cedar-lean/CedarProto/Expr.lean
+++ b/cedar-lean/CedarProto/Expr.lean
@@ -491,6 +491,12 @@ def mergeName (result : ExprKind.ExtensionFunctionApp) (xfn : Spec.Name) : BPars
     | "isLoopback" => pure $ .call .isLoopback es
     | "isMulticast" => pure $ .call .isMulticast es
     | "isInRange" => pure $ .call .isInRange es
+    | "datetime" => pure $ .call .datetime es
+    | "duration" => pure $ .call .duration es
+    | "offset" => pure $ .call .offset es
+    | "durationSince" => pure $ .call .durationSince es
+    | "toDate" => pure $ .call .toDate es
+    | "toTime" => pure $ .call .toTime es
     | xfn => throw s!"mergeName: unknown extension function {xfn}"
   | _ => panic!("Expected ExprKind.ExtensionFunctionApp to have constructor .call")
 
diff --git a/cedar-lean/CedarProto/Type.lean b/cedar-lean/CedarProto/Type.lean
index 08c80708d..8ab17e9d5 100644
--- a/cedar-lean/CedarProto/Type.lean
+++ b/cedar-lean/CedarProto/Type.lean
@@ -162,6 +162,8 @@ partial def toCedarType : ProtoType → Except String CedarType
   | .ext n => match n.id with -- ignoring n.path because currently no extension types have nonempty namespaces
     | "ipaddr" => .ok (.ext .ipAddr)
     | "decimal" => .ok (.ext .decimal)
+    | "datetime" => .ok (.ext .datetime)
+    | "duration" => .ok (.ext .duration)
     | _ => .error s!"unknown extension type name: {n.toName}"
 
 end ProtoType