4
$\begingroup$

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?

Seems 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.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ Done! You can edit the tag wiki if you like. $\endgroup$
    – Trebor ♦
    Jun 10 at 16:15
  • 1
    $\begingroup$ I’m not aware of anything like that, so I think the answer is no, but I see here Leo mentioning that this is a planned future addition to Lean (leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/…). That was over a year ago, so I’ll let a more knowledgeable person answer. $\endgroup$
    – Jason Rute
    Jun 10 at 16:22

1 Answer 1

Reset to default
6
$\begingroup$

No, the type checker implements a theory that does not have any substructural types in it. You can implement this as an after-the-fact checker though, by analyzing the term to see where it has been used.

Improve this answer
$\endgroup$
2
  • $\begingroup$ True, but I'd like to use it within proofs, to prove an algorithm uses resources according to plan. An after-the-fact checker won't interact with other proofs in LEAN I suspect. $\endgroup$
    – Algeboy
    Jun 11 at 14:06
  • 1
    $\begingroup$ It can, your after the fact checker can produce proofs of its own which interact with other proofs produced by the checker to get whole program correctness statements. It's a project, though, people usually write masters theses about this kind of thing. $\endgroup$
    – Mario Carneiro
    Jun 11 at 17:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.