search

FissoreD / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
0 stars 0 forks source link

This should pass: maybe-beta approx seems wrong #7

Closed FissoreD closed 4 months ago

FissoreD commented 4 months ago 
From elpi Require Import tc.

Class B (i: nat -> nat -> nat).

Axiom (f : nat -> nat).
Instance instB: B (fun _ _ => f 3) := {}.

Class A.
Instance instA : forall X, B (fun x => X x x) -> A := {}.

Goal A.
  Fail apply _.
Qed.
FissoreD commented 4 months ago

Solved by using @gares algo. Here the commits 3505944 and cab77a6