Fridtjof Siebert
Fridtjof Siebert
This is the underlying issue of #3613. Here is an example with unsound types ``` r(T type, v T) is A ref is f(p r A.this) b => b b...
Look at this code that defines two features `x` with two and three arguments: ``` x(T type, v T) => say "x1 $T $v" x(T type, v, w T) =>...
`infix =` currently is not applicable to `Sequence`, would be nice if it was in case `Sequence.T` is `equatable`, need to see how this could be done. See #3480.
This example defines two features `x` using an explicit type parameter and two features `y` using a free type parameter. Both declarations should be equivalent: ``` x(T type, v T)...
take this code ``` e is e.type.r e.this type.r(E type : e, v E) => f : e is _ := f ``` and run`fz` with pre/postconditions enabled, you get...
This is an open task related to #3480: More complex boolean expressions like `pre T : x && U : y` or `if !(T : x) || cc then ......
A missing part of #3480: This example ``` test(T, U type, t T, u U) is constraint(Q type) pre T : String U : Sequence Q is show => say...
`Context` should not be needed after the front end. Nevertheless, it is used in AIR and FUIR code since some method in `AbstractType` like `choiceGenerics` require a context since they...
With #3480, this is should no longer be needed, but this probably requires fixing #3544 first.
This cleanup was left after #3480