ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
18,511 Commits 65 Branches 1 Tag
master
Commit Graph

7 Commits

Author SHA1 Message Date
Guillaume Melquiond
ea123b5e95 Improve documentation of standard library. 2021-09-21 18:00:14 +02:00
Andrei Paskevich
79f564bdff WhyML: reference variables 
caveat: pass-as-reference does not work in chain relations.
        That is, 0 < r += 12 will not typecheck even
        if x is autodereferencing and (+=) has the
        first parameter with the reference marker.

todo: forbid reference markers in logic, in type definitions,
      over logical symbols, etc.

todo: update extraction drivers.
      why3.Ref.Ref defines
        - type "ref",
        - constructor "mk ref" (never used in Typing)
        - projection "contents" (both val and function)
        - program function "ref" (alias for "mk ref")
      ref.Ref defines
        - let-function (!)
        - program function (:=)

      It is important to attribute the symbols to their
      respective modules, since a program with reference
      variables may never use ref.Ref and why3.Ref.Ref
      is imported automatically.
 2018-10-21 22:15:17 +02:00
Andrei Paskevich
79923ded5e WhyML: make the ref type built-in and handle the "ref" keyword 2018-10-14 21:54:29 +02:00
Andrei Paskevich
eae547d95f stdlib, examples: remove redundant "import" 2018-06-15 16:45:58 +02:00
Guillaume Melquiond
27af960240 Avoid some backticks in documentation. 
"\`\`" could have been used too, but it is a bit unreadable.
 2018-06-14 08:14:06 +02:00
Guillaume Melquiond
9e92f8203f Change label syntax from "foo" to [@foo]. 
The feature is not yet fully implemented (e.g. escape characters).
 2018-01-12 18:05:43 +01:00
Guillaume Melquiond
efb51e7d43 Merge theories and modules into stdlib (fix issue #62). 2017-12-15 15:34:35 +01:00