Formalization work for the SMC stack [Chen2012] #540
Annotations
10 warnings
|
Run coq-community/docker-coq-action@v1:
lib/realType_ext.v#L23
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Run coq-community/docker-coq-action@v1:
lib/realType_ext.v#L27
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Run coq-community/docker-coq-action@v1:
lib/realType_ext.v#L28
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Run coq-community/docker-coq-action@v1:
lib/ssralg_ext.v#L38
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Run coq-community/docker-coq-action@v1:
lib/derive_ext.v#L5
Notations "[ fun _ => _ ]" defined at level 0 with arguments name
|
|
Run coq-community/docker-coq-action@v1:
lib/derive_ext.v#L7
Notations "{ ' _ | _ }" defined at level 0
|
|
Run coq-community/docker-coq-action@v1:
lib/derive_ext.v#L122
Argument a was previously inferred to be in scope ring_scope but is
|
|
Run coq-community/docker-coq-action@v1:
probability/fdist.v#L78
Notations "_ <| _" defined at level 70 with arguments constr
|
|
Run coq-community/docker-coq-action@v1:
probability/fdist.v#L936
Postfix notations (i.e. starting with a nonterminal symbol and
|
|
Run coq-community/docker-coq-action@v1:
probability/fdist.v#L937
Postfix notations (i.e. starting with a nonterminal symbol and
|
Loading