Skip to content
GitLab
Commit 19649432 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typo.

parent 1eba7121
Pipeline #5580 passed with stages
in 5 minutes and 50 seconds
Hide whitespace changes
Inline Side-by-side
theories/algebra/frac_auth.v
View file @ 19649432
......@@ -93,7 +93,7 @@ Section frac_auth.
IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯!{q} a) (◯!{q1} a1) (◯!{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) :
CoreId a → IsOp q q1 q2 → IsOp' (◯!{q} a) (◯!{q1} a) (◯!{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment