coq icon indicating copy to clipboard operation
coq copied to clipboard

Published 20 hours ago • verified publisher icon coq

Fixes "where notation" clause of interactive Fixpoint

Open herbelin opened this issue 1 year ago • 1 comments

The PR fixes

Fixpoint f (n:nat) : nat where "- n" := (f n).

which was failing with f not found beforehand.

  • [x] Added / updated test-suite.

herbelin avatar Mar 02 '24 14:03 herbelin

@coqbot run full ci

herbelin avatar Mar 04 '24 08:03 herbelin

@coqbot merge now

SkySkimmer avatar Mar 04 '24 13:03 SkySkimmer