search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.66k stars 418 forks source link

coinductive predicates #401

Open leodemoura opened 3 years ago

leodemoura commented 3 years ago

Port and cleanup the Lean 3 coinductive predicate meta program to Lean 4. https://github.com/leanprover-community/mathlib/blob/76a3b82dc0ae6c9a60a8714d74c6cf2b854cf17b/src/meta/coinductive_predicates.lean

digama0 commented 3 years ago

This was removed from lean 3 core a long time ago. Is there a reason it needs to be in lean 4 core? I would be inclined to just keep it as a user add-on.

One aspect where lean support may be necessary is in being able to register arbitrary types to have an "inductive-like" interface that will be used by match, cases, and inductive. This is a separate feature that requires some design work, though.