Commit 8e069e6b authored by Ralf Jung's avatar Ralf Jung
Browse files

infprod RA: explain types

parent dc078e32
......@@ -369,6 +369,7 @@ End Agreement.
Section InfiniteProduct.
(* S is the index type (domain), T the type of the components (codomain) *)
Context (S T : Type) `{RA_T : RA T}.
Local Open Scope ra_scope.
Markdown is supported
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