Zulip Chat Archive

Stream: new members

Topic: How to turn off termination checking for a function?


view this post on Zulip Marko Grdinić (Oct 27 2019 at 07:55):

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?

view this post on Zulip Kevin Buzzard (Oct 27 2019 at 08:13):

Is it meta?

view this post on Zulip Marko Grdinić (Oct 27 2019 at 08:16):

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.

view this post on Zulip Marko Grdinić (Oct 27 2019 at 08:16):

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

view this post on Zulip Marko Grdinić (Oct 27 2019 at 08:16):

Thank you, that was it.


Last updated: May 09 2021 at 19:11 UTC