You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
constant symbol Set : TYPE;
injective symbol τ : Set → TYPE;
constant symbol prop : Set;
symbol Prop ≔ τ prop;
injective symbol π : Prop → TYPE;
constant symbol ∀ {a} : (τ a → Prop) → Prop;
set quantifier ∀;
set verbose 3;
set flag "print_implicits" on;
set flag "print_domains" on;
set unif_rule π $p ≡ Π x, π $q[x] ↪ [ $p ≡ `∀ x, $q[x] ];
// (hint) [#equiv (π $v0_p) (Π x: $v1, π $v2_q[x]) ↪ #equiv $v0_p (`∀ x: {|?0|}, $v2_q[x])]
// this can later create the following error:
// Uncaught exception: File "src/core/sign.ml", line 191, characters 22-28: Assertion failed.
The text was updated successfully, but these errors were encountered:
fblanqui
changed the title
set unif_rule does not convert metavariables into pattern variables
unif_rule does not convert metavariables into pattern variables
Dec 15, 2021
The text was updated successfully, but these errors were encountered: