Improve notations for functions

We use fnrec: for recursive functions and fn: for non-recursve functions. This is both shorter and closer to Rust.

This follows a suggestion by @shiatsumat.

theories/lang/notation.v

@@ -61,10 +61,14 @@ Notation "λ: xl , e" := (Lam xl%binder e%E)
 Notation "λ: xl , e" := (locked (LamV xl%binder e%E))
   (at level 102, xl at level 1, e at level 200) : val_scope.
 
-Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
-  (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
-Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
-  (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%E
+  (at level 102, f, xl at level 1, e at level 200) : expr_scope.
+Notation "'fnrec:' f xl := e" := (rec: f (BNamed "return"::xl) := e)%V
+  (at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'fn:' xl := e" := (fnrec: <> xl := e)%E
+  (at level 102, xl at level 1, e at level 200) : expr_scope.
+Notation "'fn:' xl := e" := (fnrec: <> xl := e)%V
+  (at level 102, xl at level 1, e at level 200) : val_scope.
 Notation "'return:'" := "return" : expr_scope.
 
 Notation "'let:' x := e1 'in' e2" :=