Extremely basic refinement types in Lean 4

Stream: new members

[Malcolm Langfield]

Hi. I've got a basic question. I want to define a very basic refinement type, which is the type of all nonnegative Floats. How can I do this with inductive? Is the best way to have the type take as arguments a Float and a proof that that float is nonnegative? Could anyone please give an example? Thanks so much!

[Eric Wieser]

You probably want docs4#Subtype