Syntax for assertion

[Jimmy Johnson]

Sorry, this is basic, but even after decades with Eiffel, I never can remember how to write this.

1.  Given  my_set: SET [MY_OBJECT] and MY_OBJECT has feature is_something: BOOLEAN

how do I write an assertion stating "for all items in my list, `is_something' must be true"?

2.  What in the world do I google to find this answer for myself?  

     a.  Google always returns information about the Eiffel Tower

     b.  This list does not seem to understand regular expressions when serching

     c.  I bet Eiffel.com website has the answer somewhere ... but where?

I wonder how newbies approach this?

jjj

[Eric Bezault]

Hi Jimmy,

across my_set as obj all obj.is_something end

or:

∀ obj: my_set ¦ obj.is_something

It looks like there is no feature `for_all` in class SET.
For containers which do have this feature, you can also
write:

my_container.for_all (agent {MY_OBJECT}.is_something)

--
Eric Bezault
mailto:er...@gobosoft.com
http://www.gobosoft.com

> --
> You received this message because you are subscribed to the Google
> Groups "Eiffel Users" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to eiffel-users...@googlegroups.com <mailto:eiffel-
> users+un...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/eiffel-
> users/a553d9aa-3d5e-417b-878b-bb023bb503ben%40googlegroups.com <https://
> groups.google.com/d/msgid/eiffel-users/a553d9aa-3d5e-417b-878b-
> bb023bb503ben%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Liberty Lover]

Across Quantifiers

  For the assertion "for all items in my_set, is_something must be true":

  require
      all_are_something: across my_set as ic all ic.item.is_something end

  The key syntax is across ... all ... end (universal quantifier). There's also some for existential:

  -- At least one is_something
  some_is_something: across my_set as ic some ic.item.is_something end

  Google tips for finding this:
  - Search: "Eiffel" "across" "all" quantifier (quotes force exact matches)
  - Better: site:eiffel.org across quantifier
  - ECMA-367 spec section 8.24.8 covers this
  - OOSC2 Chapter 11 discusses quantified expressions

  Direct links:
  - https://www.eiffel.org/doc/eiffel/Across - official documentation
  - The iteration form uses loop/end, the boolean form uses all/some/end

--

You received this message because you are subscribed to the Google Groups "Eiffel Users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to eiffel-users...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/eiffel-users/a553d9aa-3d5e-417b-878b-bb023bb503ben%40googlegroups.com.

[Eric Bezault]

On 17/12/2025 0:29, Liberty Lover wrote:
> Across Quantifiers
>
>   For the assertion "for all items in my_set, is_something must be true":
>
>   require
>       all_are_something: across my_set as ic all ic.item.is_something end

This does not follow the recommendations here:

https://github.com/simple-eiffel/claude_eiffel_op_docs/blob/main/language/across_loops.md

so that Claude can convince itself that it is an expert:

~~~~
The cursor IS the item. Use the cursor directly:
~~~~

:-)

[Jimmy Johnson]

Thanks, everyone.  Nice, quick answers.  I'm writing it down.

jjj