Mentions légales du service

Skip to content
  • 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