What does `opaque` do?

Stream: new members

[Jiang Jiedong]

Hi everyone,
I was wandering in Mathlib and found that the type Float in Mathlib is formalized using many opaque and attributes like @[extern "lean_float_add"]. What do these mean? Does the attribute @[extern] link this definition to some concrete definitions and functions of float? (Maybe some float in C or some language other than Lean?) Thank you!

[Henrik Böving]

opaque tells the logic part of Lean that there exists some constant with this name and this type. Notably in order to declare an opaque its type must have at least one inhabitant to prevent unsoundness. The extern annotation can be put on any function and tells the compiler part of Lean to replace references of this function with ones to the C function mentioned in the extern

[Shreyas Srinivas]

how does opaque differ from axiom?

[Henrik Böving]

axiom does not have the inhabited condition and can thus introduce inconsistency.