Well foundedness declarations

Stream: new members

[Ken Roe]

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]

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

[Kevin Buzzard]

```lean at the beginning and ``` at the end

[Ken Roe]

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.