# \#ssreflect

**URL:** https://discourse.rocq-prover.org/tag/ssreflect/3.md

[Latest](https://discourse.rocq-prover.org/latest.md) · [Categories](https://discourse.rocq-prover.org/categories.md) · [Tags](https://discourse.rocq-prover.org/tags.md)

---

## [MathComp 2.4.0 released](https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632)

<div class="topic-metadata">

**Author:** [@CohenCyril](https://discourse.rocq-prover.org/u/CohenCyril)\
**Replies:** 0\
**Last updated:** [April 14, 2025, 3:45pm UTC](https://discourse.rocq-prover.org/t/mathcomp-2-4-0-released/2632 "2025-04-14T15:45:36Z")

</div>

We are proud to announce the immediate availability of the Mathematical Components library version 2.4.0. The webpage, and documentation, are available at https://math-comp.github.io/. This release is compatible with C…

---

## [Apply: versus apply](https://discourse.rocq-prover.org/t/apply-versus-apply/1704)

<div class="topic-metadata">

**Author:** [@nobrowser](https://discourse.rocq-prover.org/u/nobrowser)\
**Replies:** 4\
**Last updated:** [June 24, 2022, 9:10am UTC](https://discourse.rocq-prover.org/t/apply-versus-apply/1704 "2022-06-24T09:10:18Z")

</div>

I am really, really confused by the difference between the normal apply tactic and the ssreflect apply: tactic. Here’s a script, the beginning of a toy formalization of Go/Weiqi/Baduk rules. In the last proof, in the in…

---

## [Completely confused by a trivial SSR proof with case](https://discourse.rocq-prover.org/t/completely-confused-by-a-trivial-ssr-proof-with-case/1610)

<div class="topic-metadata">

**Author:** [@nobrowser](https://discourse.rocq-prover.org/u/nobrowser)\
**Replies:** 3\
**Last updated:** [March 30, 2022, 7:12am UTC](https://discourse.rocq-prover.org/t/completely-confused-by-a-trivial-ssr-proof-with-case/1610 "2022-03-30T07:12:17Z")

</div>

Given this: Inductive color := Black | White. Inductive point\_state := | Occupied of color | Empty . this works: Fact ps\_case (ps: point\_state): ps = Occupied White ∨ ps = Occupied Black ∨ ps = Empty. Pr…

---

## [« if \_ is \_ then \_ else » notation](https://discourse.rocq-prover.org/t/if-is-then-else-notation/437)

<div class="topic-metadata">

**Author:** [@lelf](https://discourse.rocq-prover.org/u/lelf)\
**Replies:** 1\
**Last updated:** [September 21, 2019, 12:07pm UTC](https://discourse.rocq-prover.org/t/if-is-then-else-notation/437 "2019-09-21T12:07:41Z")

</div>

Just out of curiosity: Require Import ssreflect. Definition foo a := if a is S \_ then true else false. Print foo. (\* foo = fun a : nat =\> match a with … \*) Import IfNotations. Definition bar a := if a is S \_ then true…