From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=3.0 tests=BAYES_40,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.6
X-Received: by 2002:a05:622a:394:: with SMTP id j20mr4591033qtx.196.1630610247233;
        Thu, 02 Sep 2021 12:17:27 -0700 (PDT)
X-Received: by 2002:a05:6902:1247:: with SMTP id t7mr5988216ybu.161.1630610246956;
 Thu, 02 Sep 2021 12:17:26 -0700 (PDT)
Path: eternal-september.org!reader02.eternal-september.org!news.mixmin.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 2 Sep 2021 12:17:26 -0700 (PDT)
In-Reply-To: <86r1e80zu2.fsf@stephe-leake.org>
Injection-Info: google-groups.googlegroups.com; posting-host=93.41.3.120; posting-account=9fwclgkAAAD6oQ5usUYhee1l39geVY99
NNTP-Posting-Host: 93.41.3.120
References: <10e82e71-53f5-46d0-8960-46a7593b964dn@googlegroups.com> <86r1e80zu2.fsf@stephe-leake.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4fc90fe9-f75e-437c-babd-05ea194d42e6n@googlegroups.com>
Subject: Re: Postcondition on Strings.Maps.To_Sequence
From: mockturtle <framefritti@gmail.com>
Injection-Date: Thu, 02 Sep 2021 19:17:27 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: reader02.eternal-september.org comp.lang.ada:62608
List-Id: <comp.lang.ada>

On Wednesday, September 1, 2021 at 11:07:41 PM UTC+2, Stephen Leake wrote:

> 
> So just guessing; does Spark actually understand 'Length? 

I think it does, since I use it frequently in contracts (e.g. putting in some procedure the pre-condition that a string must be shorter than Positive'Last since otherwise Spark complains that I could have an overflow)

> 
> For example, can it prove "a"'Length = 1? 
> and then To_Sequence (To_Set ('a'))'Length = 1?

Good idea, I'll try this test.