Stream: math-comp users

Topic: Array definition fails

view this post on Zulip Quentin Canu (Dec 09 2021 at 17:22):

Hello everyone,
it seems I can't define explicitly arrays when I import mathcomp modules
For instance, this code won't work for me

From mathcomp Require Import all_ssreflect.
From Coq Require Import PArray.

Check [| true; true | false|].

I'm getting the following message : Syntax error: 'equiv_rel' 'of' expected after '[' (in [term]).

I am understanding that it is looking for a notation, but I don't know how to handle this ?

view this post on Zulip Pierre-Yves Strub (Dec 09 2021 at 19:50):

Note that your example is working with Coq 8.14 & mathcomp 1.13.

Last updated: Jul 15 2024 at 21:02 UTC