comp.lang.ada
 help / color / mirror / Atom feed
From: "Randy Brukardt" <randy@rrsoftware.com>
Subject: Re: Record operations (Algebraic Data Types and printing)
Date: Tue, 9 Oct 2018 17:25:26 -0500
Date: 2018-10-09T17:25:26-05:00	[thread overview]
Message-ID: <ppj9sm$vq2$1@franka.jacob-sparre.dk> (raw)
In-Reply-To: 87d0sj379h.fsf@nightsong.com

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 871 bytes --]

"Paul Rubin" <no.email@nospam.invalid> wrote in message 
news:87d0sj379h.fsf@nightsong.com...
> Henrik Härkönen <heharkon@gmail.com> writes:
>> And interestingly, what got me initially checking more about Ada, was
>> this Wikipedia page about Dependent Types, where "Ada 202x" was listed
>> to be supporting those:
>>
>> https://en.wikipedia.org/wiki/Dependent_type
>
> I don't think that can be right, in the sense in which that term is
> normally used.  But, I think C++ uses it to mean something different, so
> maybe Ada 202x does as well.

The Wikipedia article references "Subtype predicates" (and I would add "Type 
invariants" to that) to provide this capability. Which means the reference 
really should be to Ada 2012, since that is where those were introduced. It 
also references SPARK to get static proofs.

                                         Randy.



  parent reply	other threads:[~2018-10-09 22:25 UTC|newest]

Thread overview: 43+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-10-05 17:46 Record operations (Algebraic Data Types and printing) Henrik Härkönen
2018-10-05 17:58 ` AdaMagica
2018-10-05 18:11   ` Henrik Härkönen
2018-10-05 18:46     ` Niklas Holsti
2018-10-05 20:33       ` Henrik Härkönen
2018-10-06  5:38   ` J-P. Rosen
2018-10-06  7:08     ` Henrik Härkönen
2018-10-06 16:42       ` Lucretia
2018-10-08 23:08         ` Randy Brukardt
2018-10-09  1:12           ` Lucretia
2018-10-09 22:20             ` Randy Brukardt
2018-10-10  7:17               ` Dmitry A. Kazakov
2018-10-10 18:13                 ` G. B.
2018-10-10 18:36                   ` Dmitry A. Kazakov
2018-10-11 11:29                   ` Björn Lundin
2018-10-11 14:45                     ` Jacob Sparre Andersen
2018-10-11 18:34                       ` Björn Lundin
2018-10-12 19:08                     ` G. B.
2018-10-12 19:20                       ` Randy Brukardt
2018-10-11 21:32                   ` Randy Brukardt
2018-10-10 18:38                 ` Shark8
2018-10-11  8:36                   ` Dmitry A. Kazakov
2018-10-11 21:35                 ` Randy Brukardt
2018-10-12  7:14                   ` Dmitry A. Kazakov
2018-10-12 19:16                     ` Randy Brukardt
2018-10-06 16:18     ` Jeffrey R. Carter
2018-10-06 17:19       ` Dmitry A. Kazakov
2018-10-08 23:03   ` Randy Brukardt
2018-10-09  6:22     ` Henrik Härkönen
2018-10-09  7:32       ` Paul Rubin
2018-10-09  7:38         ` Henrik Härkönen
2018-10-09 22:25         ` Randy Brukardt [this message]
2018-10-05 18:32 ` Niklas Holsti
2018-10-05 18:43   ` Henrik Härkönen
2018-10-05 19:41   ` Simon Wright
2018-10-06  6:17     ` Henrik Härkönen
2018-10-06 16:04       ` Stephen Leake
2018-10-06 16:56         ` Simon Wright
2018-10-08  6:44           ` briot.emmanuel
2018-10-08 14:09             ` Simon Wright
2018-10-08 14:21               ` Bill Findlay
2018-10-08 14:42                 ` Simon Wright
2018-10-08 16:46                   ` Bill Findlay
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox