mkCIdentFromRef returns untyped Syntax

Stream: lean4

[Raghuram Sundararajan]

I noticed that (on nightly-2023-02-04) while mkIdent, mkIdentFrom, mkIdentFromRef, mkCIdent and mkCIdentFrom in the Lean namespace all return typed syntax Ident (possibly in a monad), mkCIdentFromRef returns untyped Syntax, which doesn't seem to be necessary, since it simply calls mkCIdentFrom. Is this a bug?

[Mario Carneiro]

yes

[Raghuram Sundararajan]

Filed