Skip to main content

is_deprecated_alias

lean_ctx::server::dynamic_tools

Function is_deprecated_alias 

Source 
pub fn is_deprecated_alias(name: &str) -> bool
Expand description

Whether name is a deprecated alias hidden from tools/list (#509).