• MARCHE Claude's avatar
    ITP: support for qualified ident and infix ident · bccdfacc
    MARCHE Claude authored
    command "search" and transformations taking idents as arguments now can
    support qualified idents and infix symbols.
    
    For example, "search (+) (*)" returns the distributivity axioms
    
    FIXME: "search Int.(+)" fails, probably missing namespaced for
    imported modules
    bccdfacc
lexer.mll 7.53 KB