CODEWITHSUNDEEP
lean
Sven Williamson
Sven Williamson

Reputation: 1124

What is the equivalent of Coq's 'fix' keyword to create fixpoints in Lean

I am trying to make literal translation of Coq terms into Lean terms but realize I am not aware of how to translate the Coq primitive fix as in:

Definition Fac : nat -> nat :=
    fix f (n:nat) : nat :=
        match n with
        | 0     => 1
        | S p   => S p * f p
        end.

I am not asking about how to define recursive functions on inductive types which is well explained in the Lean documentation, but rather how to define 'recursive lets', i.e. lambda abstraction whose body calls itself. I assume an equivalent primitive exists in Lean.

Thank you.

Upvotes: 0

Views: 351

Answers (1)

Christopher Hughes
Christopher Hughes

Reputation: 1129

There's a discussion about this here. As far as I know there isn't nice notation for it.

The closest you can get is to use the recursor for nat directly, or well_founded.fix directly.

e.g

def fact (n : ℕ) : ℕ :=
let f : ℕ → ℕ := λ n, nat.rec_on n 1 (λ n fact, (n + 1) * fact) in
f n

or

def fact' (n : ℕ) : ℕ :=
let f : ℕ → ℕ := λ n, well_founded.fix nat.lt_wf 
  (λ n fact, show ℕ, from nat.cases_on n (λ _, 1)
    (λ n fact, (n + 1) * fact n n.lt_succ_self) fact) 
  n in
f n

Upvotes: 1

Related Questions