# Zulip Chat Archive

## Stream: general

### Topic: anonymous recursive functions

#### Andrew Ashworth (Jun 17 2018 at 04:31):

is it possible to define an anonymous recursive function? so for I've been making auxiliary defs as needed, but I'm copying a development from coq that uses them a lot

#### Andrew Ashworth (Jun 17 2018 at 04:32):

something like this from CPDT

Definition check_even : forall n : nat, [isEven n]. Hint Constructors isEven. refine (fix F (n : nat) : [isEven n] := match n with | 0 => Yes | 1 => No | S (S n') => Reduce (F n') end); auto. Defined.

#### Mario Carneiro (Jun 17 2018 at 05:46):

Unfortunately no, at least not in term mode. As a workaround you can use `induction`

, but the only way to get the full power of the equation compiler is to have an auxiliary def, and this is what I usually do.

#### Simon Hudon (Jun 17 2018 at 13:12):

You could write

nat.rec Yes (λ f n, match n with | 0 := No | (succ n') := Reduce (f n') end )

#### Mario Carneiro (Jun 17 2018 at 17:30):

There is also a somewhat hackish way. Did you ever wonder about those `_match`

and `_let_match`

variables in the context sometimes? Those are the same mechanism used to support recursive definitions using the equation compiler, and if you refer to them it will get compiled to a recursive function just like a recursive def. For example:

def fib (n : ℕ) : ℕ := match n with | 0 := 0 | 1 := 1 | n+2 := by rename _match fib; exact fib n + fib (n+1) end

This doesn't work in term mode though:

def fib (n : ℕ) : ℕ := match n with | 0 := 0 | 1 := 1 | n+2 := _match n + _match (n+1) end

fails unless you insert `by exact`

on the last line.

#### Mario Carneiro (Jun 17 2018 at 17:42):

I guess the main reason this isn't already supported officially is because there is no obvious place in match notation to put the name of the defined function

#### Mario Carneiro (Jun 17 2018 at 17:51):

Examples of the other two match types:

inductive tree : Type | mk : ∀ n, (fin n → tree) → tree def path : tree → Type := λ ⟨n, t⟩, by exact Σ n, _fun_match (t n) def path' (T : tree) : Type := let ⟨n, t⟩ := T in by exact Σ n, _let_match (t n)

#### Simon Hudon (Jun 17 2018 at 17:53):

Cool hack :grin:

Last updated: May 08 2021 at 09:11 UTC