## Stream: new members

### Topic: Well foundedness declarations

#### Ken Roe (Jul 11 2018 at 15:44):

It seems for the mutually recursive function below, Lean cannot find the well founded relation. How can I specify the relation?

inductive Value : Type
| NatValue : ℕ -> Value
| ListValue : list Value -> Value
| NoValue : Value

mutual def findRecord, findRecordHelper
with findRecord : ℕ → Value → (list Value)
| l (Value.ListValue ((Value.NatValue x)::r)) :=
if beq_nat x l then
((Value.NatValue x)::r)
else findRecordHelper x r
| _ _ := list.nil
with findRecordHelper : ℕ → (list Value) → (list Value)
| _ list.nil := list.nil
| v (f::r) := match findRecord v f with
| list.nil := findRecordHelper v r
| x := x
end.

#### Kevin Buzzard (Jul 11 2018 at 15:51):

Do you know about the triple back tick thing? It makes code much easier to read

#### Kevin Buzzard (Jul 11 2018 at 15:51):

 lean  at the beginning and    at the end

#### Ken Roe (Jul 11 2018 at 15:52):

Here it is with the triple back thing.

inductive Value : Type
| NatValue : ℕ -> Value
| ListValue : list Value -> Value
| NoValue : Value

mutual def findRecord, findRecordHelper
with findRecord : ℕ → Value → (list Value)
| l (Value.ListValue ((Value.NatValue x)::r)) :=
if beq_nat x l then
((Value.NatValue x)::r)
else findRecordHelper x r
| _ _ := list.nil
with findRecordHelper : ℕ → (list Value) → (list Value)
| _ list.nil := list.nil
| v (f::r) := match findRecord v f with
| list.nil := findRecordHelper v r
| x := x
end.


Last updated: May 16 2021 at 20:13 UTC