Zulip Chat Archive

Stream: lean4

Topic: Recursive definition fails


Raghuram (Oct 01 2022 at 07:40):

Why does the first definition of trans below fail, but the second succeed?

inductive TransClosure (r : α  α  Prop) : α  α  Prop
| extends : r a b  TransClosure r a b
| trans_left : r a b  TransClosure r b c  TransClosure r a c

def trans' {a b c} : TransClosure r a b  TransClosure r b c  TransClosure r a c
| .extends h₁       => .trans_left h₁
| .trans_left h₁ h₂ => .trans_left h₁  trans' h₂

def trans {a b c} : TransClosure r a b  TransClosure r b c  TransClosure r a c := by
  intro h₁; induction h₁
  case «extends» h₁       => exact .trans_left h₁
  case trans_left h₁ _ h => exact .trans_left h₁  h

(#eval Lean.versionString: 4.0.0-nightly-2022-09-29, in case this is a bug.)

Leonardo de Moura (Oct 01 2022 at 14:46):

Created an issue for it: https://github.com/leanprover/lean4/issues/1672

Daniel Fabian (Oct 02 2022 at 14:09):

feel free to track the progress on github for more in-depth discussions.


Last updated: Dec 20 2023 at 11:08 UTC