partialFixpointursion

Stream: lean4

[Robin Arnez]

I just found this:

def hello (x : Nat) : Nat := hello (x + 1)
termination_by partialFixpointursion

which seems to be treated as a special case (try changing partialFixpointursion to something else).
This seems to be some kind of leftover from testing perhaps. I love myself some "partialFixpointursion" lol

[Mario Carneiro]

the culprit is here

[Mario Carneiro]

cc: @Joachim Breitner

[Robin Arnez]

Yeah I honestly only found this because of looking in the source code

[Joachim Breitner]

:man_facepalming:

[Joachim Breitner]

What's the emoji for hiding in a cave?

[Joachim Breitner]

PR welcome :-D

[Joachim Breitner]

(I wonder if I can blame the horrible interaction of u and Ctrl-Z when using VSCode with vim bindings.)

[Patrick Massot]

This was the main reason why I gave up on vim plugins in VSCode during the dark ages before lean.nvim. Of course now the issue is completely solved by lean.nvim.

[Patrick Massot]

And don’t forget to also use something like https://github.com/debugloop/telescope-undo.nvim

[Jz Pan]

What's worse:

theorem hello (x : Nat) : False := hello (x + 1)
termination_by partialFixpointursion

[Aaron Liu]

Why is this worse? You see the same behavior when you put something else there.

[Jz Pan]

Oh sorry. I was thinking that it will get compiled... Seems that it reports the same error with OP's test code.

[Jz Pan]

I was thinking that it was the cheat code to bypass termination_by check

[Mario Carneiro]

it is a cheat code which takes you straight to the "you lose" screen

[Joachim Breitner]

A Bit Like
https://pbs.twimg.com/media/EWsJLGWXsAIhb0h?format=jpg&name=4096x4096