I think it is something like Hoogle for haskell but instead of looking for the types of the functions you look for a hash of some kind of canonical encoding of

I think it is something like Hoogle for haskell but instead of looking for the types of the functions you look for a hash of some kind of canonical encoding of the definition, so it is like an encoded knowledge graph but you should have to give rules in order to construct that graph in a canonical way. Edited: What I thought was wrong, anyway the idea of above could be useful for something like copilot to complete definitions.