 Ariadne Devos
|
3ad28c4ba8
Note what work on arrows has been performed
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
f43ea0588e
Define lifts of arrows
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
b4a48710d5
Do arrows step by step: no lifting, no Hoare
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
b14392c5f4
Let parA take implicit type parameters
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
afdcd3bc1a
Define some glue arrows
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
92079de86f
Correct definition of guarantee for sequential composition
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
05fb3e50e9
Integrate the seperate function lifting
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
faa972d9a7
Lift Gallina functions to their Arrow signatures
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
dfc0f80d88
Establish the notion of signature
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
58d76afac4
Define equivalency of arrow signatures
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
37b2b015b3
Declare composition and pure arrows
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
17bea113ea
Formulate a flawed rule for parallel composition
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
3d96f09511
Integrate sequential compatibility criterium intto seq_sig
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
219f614116
Formulate a rule for sequencing arrows
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
ad44ce431c
Give the expected signature of the sequential composition of arrows
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
b431acd847
Make ArrowSig more expressive
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
111f84c9d3
Partially formalise Arrows
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
da5b83fb87
Try formalising applicative functors
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
35fd611d27
Merge branch 'verification/positional' into formality
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
9c813b50ea
Conclude formalising number parsers
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
ece50b41b7
Define the value of positional numbers
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
89e87ff4fc
Define vector-wide bounds
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
be5bc4d224
Generate indices in a vector
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
60e3a469b7
Fold vectors, modulo an equivalence
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
c14827cd87
Try formalising a number parser
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
b432b462b3
Merge branch 'verification/language' into formality
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
df55ba65c7
Check-off regular expressions
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
6861f2e1c0
Delete unused formalisations
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
03ebdd14a7
Implement a Kleene closure
|
%!s(int64=5) %!d(string=hai) anos |
|
Ariadne Devos
|
ce76c61e33
Allow repetition of languages by a constant natural
|
%!s(int64=5) %!d(string=hai) anos |
