repos / jolie.agda.git

Add type preservation cases

Cosmetic changes

Rename file and add remaining rules

Add semantics rules for behavioural layer.

Update typing rules for network and service layers.

Replace context's constructors and add new theorems.

Edit expr

Update struct theorems and typing rules for network and service layers

Add typing rules for cases with disjoint union

Make contexts great again

Expand behaviour's typing rules. Add network and service typing rules.

Add t-bsl-choice

Rename side effect. Add comments.

Added t-mutate

Added typingnetwork

Change to unicode syntax for behaviour

Clean up

Added disjoint union

Add typing service.

Rename typecheck to typingbehaviour

Update type rules of behaviour layer.

Change direction to theorems. Add t-wait and t-exec.

...

Add t-choice case.

in work

Add context equality

Replace lemmas with lambdas

Add 'if case' to check-B

Inline substCtx

Fix equality of contexts

Merge pull request #1 from ak3n/in_types

In types version

Update service

Simplified variables and finished typing rules for behaviour.

Add t-assign-new

Add condition for t-par

Add t-notification

Express typing rules in types

TypeTree yes case

First steps with Equality

Add type_of_value and type_of_var. Remove maybe from if-then-else behaviour.

Add check type for behaviour

Fix binary expr

Add Network, Queue and Service.

Add one possible variant

Create README.md

init

Initial commit