Function test_implicit_insertion

leanr-elab/src/implicit.rs:52–57

()

    #[test]
    fn test_implicit_insertion() {
        let mctx = MetaVarContext::new();
        let handler = ImplicitHandler::new(mctx);

        // TODO: Add tests
    }
}