Scheme#

Ltac2.Scheme

type kind

An abstract type representing a scheme kind. Use the predefined values below to refer to specific scheme kinds.

  • since 9.3
val lookup : kind -> reference -> reference option

lookup kind ref looks up the scheme registered under kind for the reference ref. Returns None if ref is not an inductive type or if no such scheme is registered.

  • since 9.3

Elimination schemes#

val rect_dep : kind

Dependent recursion scheme for Type.

  • since 9.3
val rec_dep : kind

Dependent recursion scheme for Set.

  • since 9.3
val ind_dep : kind

Dependent induction scheme for Prop.

  • since 9.3
val sind_dep : kind

Dependent induction scheme for SProp.

  • since 9.3
val rect_nodep : kind

Non-dependent recursion scheme for Type.

  • since 9.3
val rec_nodep : kind

Non-dependent recursion scheme for Set.

  • since 9.3
val ind_nodep : kind

Non-dependent induction scheme for Prop.

  • since 9.3
val sind_nodep : kind

Non-dependent induction scheme for SProp.

  • since 9.3

Case analysis schemes#

  • since 9.3
val case_dep : kind

Dependent case analysis scheme for Type.

  • since 9.3
val case_nodep : kind

Non-dependent case analysis scheme for Type.

  • since 9.3
val casep_dep : kind

Dependent case analysis scheme for Prop.

  • since 9.3
val casep_nodep : kind

Non-dependent case analysis scheme for Prop.

  • since 9.3
val scase_dep : kind

Dependent case analysis scheme for SProp.

  • since 9.3
val scase_nodep : kind

Non-dependent case analysis scheme for SProp.

  • since 9.3

Equality schemes#

val sym : kind

Symmetry scheme.

  • since 9.3
val sym_involutive : kind

Involutive symmetry scheme.

  • since 9.3
val rew : kind

Right-to-left rewriting scheme.

  • since 9.3
val rew_dep : kind

Right-to-left dependent rewriting scheme.

  • since 9.3
val rew_fwd_dep : kind

Right-to-left forward dependent rewriting scheme.

  • since 9.3
val rew_r : kind

Left-to-right rewriting scheme.

  • since 9.3
val rew_r_dep : kind

Left-to-right dependent rewriting scheme.

  • since 9.3
val rew_fwd_r_dep : kind

Left-to-right forward dependent rewriting scheme.

  • since 9.3
val congr : kind

Congruence scheme.

  • since 9.3

Boolean equality and decidability schemes#

val beq : kind

Boolean equality scheme.

  • since 9.3
val dec_bl : kind

Boolean to Leibniz equality scheme.

  • since 9.3
val dec_lb : kind

Leibniz to Boolean equality scheme.

  • since 9.3
val eq_dec : kind

Decidable equality scheme.

  • since 9.3