How to turn off termination checking for a function?

Stream: new members

[Marko Grdinić]

Idris has partial annotations. Agda has the {-# TERMINATING #-} pragma. I think I saw that Lean has something like this in one of the threads, but I cannot find it. What was it?

[Kevin Buzzard]

Is it meta?

[Marko Grdinić]

Do you mean something like @[meta] def dudo.main : Particle Die → Particle Die → list AllowedClaim → state rat? No, it says that it is an unknown attribute.

[Marko Grdinić]

Ah it works like...meta def dudo.main : Particle Die → Particle Die → list AllowedClaim → state rat.

[Marko Grdinić]

Thank you, that was it.