Open artagnon opened 2 years ago
Name of the lexer Coq
Code sample
(* Now the negative universal property. *) Definition prod_coind_uncurried `{A : X -> Type} `{B : X -> Type} : (forall x, A x) * (forall x, B x) -> (forall x, A x * B x) := fun fg x => (fst fg x, snd fg x).
Description Backticks highlighted like errors.
Name of the lexer Coq
Code sample
Description Backticks highlighted like errors.