From Equations Require Export Equations.

Inductive type : Set :=
| Base
| Arrow (t1 t2 : type).
(**[]*)

Declare Scope ty_scope.
Delimit Scope ty_scope with ty.
Notation "⊥" := Base (at level 0) : ty_scope.
Notation "t1 '→' t2" := (Arrow t1 t2) (at level 5, right associativity) : ty_scope.
Open Scope ty_scope.

Reserved Notation "Γ '⊢' τ" (at level 80, no associativity).

Inductive term (Γ : list type) : type → Set :=
| Id (n : ℕ) (τ : type) :
    nth_error Γ n = Some τ →
    Γ ⊢ τ
| Abs (τ τ' : type) :
    τ ∷ Γ ⊢ τ' →
    Γ ⊢ τ → τ'
| App (τ τ' : type) :
    Γ ⊢ τ → τ' →
    Γ ⊢ τ →
    Γ ⊢ τ'
where "Γ '⊢' τ" := (term Γ τ) : type_scope.

Derive Signature for term.
Equations Derive NoConfusion NoConfusionHom Subterm for type.

Equations Derive NoConfusion NoConfusionHom Subterm for term.

Error: Anomaly "File "kernel/inductive.ml", line 431, characters 13-19: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

$ coqc -v
The Coq Proof Assistant, version 8.15.0
compiled with OCaml 4.13.1
$ opam show coq-equations -v
<><> coq-equations: information on all versions <><><><><><><><><><><><><><>  🐫
name                   coq-equations
all-installed-versions 1.3+8.13 [coq-8.13.0]  1.3+8.15 [coq-8.15]
all-versions           1.0~beta2  1.0~beta2+8.7  1.0  1.0+8.7  1.0+8.8  1.1+8.8  1.2~beta2+8.8  1.2~beta2+8.9  1.2~beta+8.8
                       1.2~beta+8.9  1.2+8.8  1.2+8.9  1.2+8.10  1.2.1+8.9  1.2.1+8.10  1.2.1+8.11  1.2.2+8.11  1.2.3+8.11
                       1.2.3+8.12  1.2.3+8.13  1.2.4+8.11  1.2.4+8.12  1.2.4+8.13  1.3~beta1+8.13  1.3~beta2+8.13  1.3+8.13
                       1.3+8.14  1.3+8.15

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫
version       1.3+8.15
repository    coq-released
url.src:      "https://github.com/mattam82/Coq-Equations/archive/refs/tags/v1.3-8.15.tar.gz"
homepage:     "https://mattam82.github.io/Coq-Equations"
bug-reports:  "https://github.com/mattam82/Coq-Equations/issues"
dev-repo:     "git+https://github.com/mattam82/Coq-Equations.git"
authors:      "Matthieu Sozeau <matthieu.sozeau@inria.fr>"
              "Cyprien Mangin <cyprien.mangin@m4x.org>"
maintainer:   "matthieu.sozeau@inria.fr"
license:      "LGPL-2.1-or-later"
tags:         "keyword:dependent pattern-matching"
              "keyword:functional elimination"
              "category:Miscellaneous/Coq Extensions"
              "logpath:Equations"
depends:      "coq" {>= "8.15" & < "8.16~"} "ocamlfind" {build}
synopsis      A function definition package for Coq
description   Equations is a function definition plugin for Coq, that allows the
              definition of functions by dependent pattern-matching and well-founded,
              mutual or nested structural recursion and compiles them into core
              terms. It automatically derives the clauses equations, the graph of the
              function and its associated elimination principle.

Derive Signature for term.
Set Debug "backtrace".
Equations Derive NoConfusion NoConfusionHom Subterm for term.

Error:
Anomaly
"File "kernel/inductive.ml", line 431, characters 13-19: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Inductive.contract_case in file "kernel/inductive.ml", line 431, characters 13-52
Called from EConstr.contract_case in file "engine/eConstr.ml", line 406, characters 35-81
Called from Inductiveops.make_case_or_project in file "pretyping/inductiveops.ml", line 389, characters 12-77
Called from Noconf.derive_no_confusion.(λ) in file "src/noconf.ml", line 127, characters 12-292
Called from Noconf.mkcase.(λ) in file "src/noconf.ml", line 43, characters 16-50
Called from CArray.map2_i in file "clib/cArray.ml", line 346, characters 30-59
Called from Noconf.mkcase in file "src/noconf.ml", line 36, characters 4-571
Called from Noconf.derive_no_confusion in file "src/noconf.ml", line 121, characters 6-728
Called from Ederive.derive_one.(λ) in file "src/ederive.ml", line 85, characters 15-29
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Vernacextend.vtmodifyprogram.(λ) in file "vernac/vernacextend.ml", line 191, characters 29-34
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(λ) in file "vernac/vernacinterp.ml", line 203, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(λ) in file "vernac/vernacinterp.ml", line 253, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 251, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(λ) in file "stm/stm.ml", line 2178, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2320, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2421, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 123, characters 2-60
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 415, characters 17-62
Called from Coqloop.read_and_execute_base in file "toplevel/coqloop.ml", line 452, characters 4-39
Called from Coqloop.read_and_execute in file "toplevel/coqloop.ml", line 458, characters 6-34

Inductive type : Set :=
| Base
| Arrow (t1 t2 : type).
(**[]*)

Equations Derive NoConfusion NoConfusionHom Subterm for type.

Declare Scope ty_scope.
Delimit Scope ty_scope with ty.
Notation "⊥" := Base (at level 0) : ty_scope.
Notation "t1 '→' t2" := (Arrow t1 t2) (at level 5, right associativity) : ty_scope.
Open Scope ty_scope.

Reserved Notation "Γ '⊢' τ" (at level 80, no associativity).

Fixpoint Has {A : Set} (a : A) (Γ : list A) : Set :=
  match Γ with
  | []    ⇒ Empty_set
  | h ∷ Δ ⇒ ((h = a) + Has a Δ)%type
  end.

Inductive term (Γ : list type) : type → Set :=
| Id (τ : type) :
  Has τ Γ →
  Γ ⊢ τ
| Abs (τ τ' : type) :
  τ ∷ Γ ⊢ τ' →
  Γ ⊢ τ → τ'
| App (τ τ' : type) :
  Γ ⊢ τ → τ' →
  Γ ⊢ τ →
  Γ ⊢ τ'
where "Γ '⊢' τ" := (term Γ τ) : type_scope.

Derive Signature for term.
Equations Derive NoConfusion NoConfusionHom Subterm for term.

Inductive term : list type → type → Set :=
| Id (Γ : list type) (τ : type) :
  Has τ Γ →
  Γ ⊢ τ
| Abs (Γ : list type) (τ τ' : type) :
  τ ∷ Γ ⊢ τ' →
  Γ ⊢ τ → τ'
| App (Γ : list type) (τ τ' : type) :
  Γ ⊢ τ → τ' →
  Γ ⊢ τ →
  Γ ⊢ τ'
where "Γ '⊢' τ" := (term Γ τ) : type_scope.

Derive Signature for term.
Equations Derive NoConfusion NoConfusionHom Subterm for term.