if syntax

Following https://github.com/rocq-prover/rocq/wiki/Rocq-Call-2026-03-17 it was agreed that the current if <term : inductive_with_two_constructos> then term else term syntactic sugar for match should be deprecated (except for (things coercible to) bool). Potential replacements are gathered here. Please list offers below, with perceived pros and cons, and historical use if any. Please try to keep the "positive" and "negative" offers in the same order when there is a correspondance

Positive case (bindings in first branch)

• No replacement, just deprecate if <term : inductive_with_two_constructors> in favor of existing match

• if <term> is <pattern> then <term> else <term>

  • already used in MathComp ecosystem
  • one of the syntax considered for the C++ standard (c.f., https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p2392r3.pdf , with context sensitive keyword is )
  • pros:
    • short
    • reads like a sentence
    • <term> and <pattern> in same order as match <term> with <pattern>
    • extensible to multiple matches by repeating " is " with some separator
  • cons:
    • requires making is a keyword (but CI https://github.com/rocq-prover/rocq/pull/21609 seems to indicate no dramatic effect, except for UniMath that is using is extensively as a variable name)
    • even when is is a keyword, it may not be clear to readers that it is a binding keyword
    • even when is is known to be a binding keyword, it is not clear from syntax which side has the binders ("is" reads like a symmetric relation)
    • directly confusable for a pointer-equality test a la Python (but pointer equality is not exposed in Rocq)
    • directly confusable for equality comparison
    • pattern (with bindings) deferred until after (which may be large)
    • see also Rust discussion ultimately rejecting this option

• if <term> .is. <pattern> then <term> else <term> (or other variants like if <term> \is <pattern>...)

  • used in Ada
  • pros:
    • <term> and <pattern> in same order as match <term> with <pattern>
    • extensible to multiple matches by repeating " .is. " with some separator
  • cons:
    • longer
    • breaks reading
    • requires making .is. a keyword (but maybe absolutely nobody uses it yet?)
    • pattern (with bindings) deferred until after (which may be large)

• if let <pattern> := <term> then <term> else <term>

  • used in Rust and Lean
  • pros:
    • no new keyword
    • bindings before terms and cases
    • Was chosen for Rust after a 373-answer survey found it twice as liked and three times less disliked than is
    • extensible to multiple matches by repeating "let := " with some separator ("&&" in Rust, chosen over ",")
  • cons:
    • let currently indicates an irrefutable pattern, not a switch
    • longer (starts with two keywords)
    • <term> and pattern> in reversed order with respect to the unsugared match construct
    • common prefix with eg if let x := tt in true then ... else ... (which is currently accepted)

• if <pattern> := <term> then <term> else <term>

  • pros:
    • short
    • no new keyword
    • starts with just one keyword
    • bindings before terms and cases
  • cons:
    • "" being a pattern is not obvious, especially extending to multiple matches with a simple separator
    • <term> and pattern> in reversed order with respect to the unsugared match construct
    • the grammar may be unexpected to those not familiar with it
    • grammar conflicts with boolean if <term>

• match <term> with <pattern> then <term> else <term>

  • pros:
    • no new keyword
    • straightforwardly extensible to multiple matches following current conventions (comma-separated terms followed by comma-separated patterns)
  • cons:
    • longer keywords
    • bindings deferred until after potentially large term

• if <term> match <pattern> then <term> else <term>

  • one of the syntax considered for the C++ standard (the other one uses context-sensitive keywords is and as)
  • pros:
    • no new keyword
    • potentially extensible to multiple matches by repeating " match "
  • cons
    • Rocq already allows match in argument position (contrarily to OCaml where it is a syntax error), so this is slightly ambiguous
    • longer
    • pattern with bindings deferred until after term (which may be large)
    • may feel a bit strange to reuse the match keyword with the role of the with keyword in match-with construct

Negative case (bindings in second branch)

• if <term> isn't <pattern> then <term> else <term>

  • already used in MathComp ecosystem
  • pros:
    • short
    • reads like a sentence
    • <term> and <pattern> in same order as match <term> with <pattern>
  • cons:
    • bindings in second branch may not be obvious
    • bindings deferred until after term (which may be large)
    • requires making isn't a keyword (though CI seems to indicate nobody uses it)
    • isn't would be the only keyword with ' in it and may not be recognized as one (especially by people not used to ' in identifiers)

• unless <term> is <pattern> then <term> else <term>

  • pros:
    • "the pattern matching clause is still framed positively, so it restores, in my mind, the idea that some new variables are bound."
    • reads like a sentence
    • <term> and <pattern> in same order as match <term> with <pattern>
  • cons:
    • requires making unless a keyword
    • not clear from reading which branch has bindings
    • bindings deferred until after term (which may be large)

• let <pattern> := <term> else <term> in <term>

  • similar to Rust
  • pros:
    • indentation would be nice when used in sequence or with a large second branch
    • bindings come before potentially large term
    • when in is the end of a line, the "error-handling" part between else and in is easy to skip
  • cons:
    • let currently indicates an irrefutable pattern, not a switch

• if <term> is <pattern> else <term> then <term>

  • pros:
    • short
    • symmetric to if <term> is <pattern> then <term> else <term>
    • avoids potentially surprising '-containing keyword compared to isn't
  • cons:
    • bindings in second branch may not be obvious
    • same other cons as if <term> is <pattern> then <term> else <term>

• let <pattern> := term | <term_else> in <term>

  • Similar to Lean (; vs in)
  • Used in Bedrock2 ecosystem, though not pervasive
  • pros:
    • short
    • bindings are obvious and first
    • no new keyword
    • when in is the end of a line, the "error-handling" part between | and in is easy to skip
  • cons:
    • let has been for single-case matches only so far, this proposal would change it to do multi-case matches