Is the LEAN type checker able to count the number of times a parameter is used in a function body?
In Idris2 for comparison I might use
(1 x:Nat) which then makes sure my function uses x exactly once. Or I might write
(0 pf: x < 5) to make sure the parameter gets erased. In LEAN can I force the type checker to counter uses?
linear-type is not a tag yet and I haven't the points needed to create a tag, happy to have a power user edit that.