()
| 132 | |
| 133 | #[test] |
| 134 | fn meta_nested_name() { |
| 135 | let id = KId::<Meta>::new(mk_addr("x"), mk_name("Lean.Parser.Term.app")); |
| 136 | let s = format!("{id}"); |
| 137 | assert!(s.starts_with("Lean.Parser.Term.app@"), "got '{s}'"); |
| 138 | } |
| 139 | |
| 140 | #[test] |
| 141 | fn meta_single_component_name() { |