def MLIR.EDSL.«uniform_opLlvm.return» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.return» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.return» 1024 (Lean.ParserDescr.symbol "llvm.return")

def MLIR.EDSL.«uniform_opLlvm.copy» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.copy» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.copy» 1024 (Lean.ParserDescr.symbol "llvm.copy")

def MLIR.EDSL.«uniform_opLlvm.neg» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.neg» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.neg» 1024 (Lean.ParserDescr.symbol "llvm.neg")

def MLIR.EDSL.«uniform_opLlvm.not» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.not» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.not» 1024 (Lean.ParserDescr.symbol "llvm.not")

def MLIR.EDSL.«uniform_opLlvm.and» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.and» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.and» 1024 (Lean.ParserDescr.symbol "llvm.and")

def MLIR.EDSL.«uniform_opLlvm.ashr» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.ashr» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.ashr» 1024 (Lean.ParserDescr.symbol "llvm.ashr")

def MLIR.EDSL.«uniform_opLlvm.or» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.or» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.or» 1024 (Lean.ParserDescr.symbol "llvm.or")

def MLIR.EDSL.«uniform_opLlvm.sdiv» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.sdiv» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.sdiv» 1024 (Lean.ParserDescr.symbol "llvm.sdiv")

def MLIR.EDSL.«uniform_opLlvm.lshr» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.lshr» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.lshr» 1024 (Lean.ParserDescr.symbol "llvm.lshr")

def MLIR.EDSL.«uniform_opLlvm.srem» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.srem» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.srem» 1024 (Lean.ParserDescr.symbol "llvm.srem")

def MLIR.EDSL.«uniform_opLlvm.udiv» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.udiv» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.udiv» 1024 (Lean.ParserDescr.symbol "llvm.udiv")

def MLIR.EDSL.«uniform_opLlvm.urem» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.urem» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.urem» 1024 (Lean.ParserDescr.symbol "llvm.urem")

def MLIR.EDSL.«uniform_opLlvm.xor» : Lean.ParserDescr

Equations

• MLIR.EDSL.«uniform_opLlvm.xor» = Lean.ParserDescr.node `MLIR.EDSL.«uniform_opLlvm.xor» 1024 (Lean.ParserDescr.symbol "llvm.xor")

def MLIR.EDSL.«overflow_opLlvm.add» : Lean.ParserDescr

Equations

• MLIR.EDSL.«overflow_opLlvm.add» = Lean.ParserDescr.node `MLIR.EDSL.«overflow_opLlvm.add» 1024 (Lean.ParserDescr.symbol "llvm.add")

def MLIR.EDSL.«overflow_opLlvm.shl» : Lean.ParserDescr

Equations

• MLIR.EDSL.«overflow_opLlvm.shl» = Lean.ParserDescr.node `MLIR.EDSL.«overflow_opLlvm.shl» 1024 (Lean.ParserDescr.symbol "llvm.shl")

def MLIR.EDSL.«overflow_opLlvm.mul» : Lean.ParserDescr

Equations

• MLIR.EDSL.«overflow_opLlvm.mul» = Lean.ParserDescr.node `MLIR.EDSL.«overflow_opLlvm.mul» 1024 (Lean.ParserDescr.symbol "llvm.mul")

def MLIR.EDSL.«overflow_opLlvm.sub» : Lean.ParserDescr

Equations

• MLIR.EDSL.«overflow_opLlvm.sub» = Lean.ParserDescr.node `MLIR.EDSL.«overflow_opLlvm.sub» 1024 (Lean.ParserDescr.symbol "llvm.sub")

def Lean.Parser.Category.InstCombine.cmp_op_name : Lean.Parser.Category

Equations

• Lean.Parser.Category.InstCombine.cmp_op_name = { }

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.eq» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.eq» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.eq» 1024 (Lean.ParserDescr.symbol "llvm.icmp.eq")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.ne» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.ne» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.ne» 1024 (Lean.ParserDescr.symbol "llvm.icmp.ne")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.slt» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.slt» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.slt» 1024 (Lean.ParserDescr.symbol "llvm.icmp.slt")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.sle» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.sle» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.sle» 1024 (Lean.ParserDescr.symbol "llvm.icmp.sle")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.sgt» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.sgt» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.sgt» 1024 (Lean.ParserDescr.symbol "llvm.icmp.sgt")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.sge» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.sge» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.sge» 1024 (Lean.ParserDescr.symbol "llvm.icmp.sge")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.ult» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.ult» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.ult» 1024 (Lean.ParserDescr.symbol "llvm.icmp.ult")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.ule» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.ule» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.ule» 1024 (Lean.ParserDescr.symbol "llvm.icmp.ule")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.ugt» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.ugt» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.ugt» 1024 (Lean.ParserDescr.symbol "llvm.icmp.ugt")

def MLIR.EDSL.«cmp_op_nameLlvm.icmp.uge» : Lean.ParserDescr

Equations

• MLIR.EDSL.«cmp_op_nameLlvm.icmp.uge» = Lean.ParserDescr.node `MLIR.EDSL.«cmp_op_nameLlvm.icmp.uge» 1024 (Lean.ParserDescr.symbol "llvm.icmp.uge")

def MLIR.EDSL.«mlir_op_=__,_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def MLIR.EDSL.«mlir_op_=Llvm.mlir.constant(_:_):_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def MLIR.EDSL.«mlir_op_=Llvm.mlir.constant($_{_}):_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def MLIR.EDSL.«mlir_op_=Llvm.mlir.constant_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def MLIR.EDSL.«mlir_op_=Llvm.mlir.constant$_{_}:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def MLIR.EDSL.«mlir_op_=Llvm.select_,_,_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

antiquotations test