Zulip Chat Archive

Stream: new members

Topic: Well foundedness declarations


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 15:51):

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

view this post on Zulip Kevin Buzzard (Jul 11 2018 at 15:51):

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

view this post on Zulip 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