Commits on Aug 24, 2020

1. Remove T_abs with (Path = T_sub) and add T_abs & T_sub syntax... …

   ...for type refinement.
   
   The new
   
       T_abs & T_sub
   
   mechanism is similar to the old
   
       T_abs with (Path = T_sub)
   
   mechanism and also to the include mechanism
   
       {...T_abs; ...T_sub}
   
   The main difference is that, instead of using a path to target a specific
   substructure or requiring that no declarations overlap, an intersection,
   `T_int`, of the nested declarations of `T_abs` and `T_sub`, is computed.
   
   Then it is checked whether `T_abs :> T_int` and if so a substitution, `𝛿`, is
   obtained.  Finally the nested declarations of `𝛿(T_abs)` and `T_sub` are merged.
   
   Also, in `T1 & T2` both `T1` and `T2` are elaborated in the same environment
   whereas in `{...T1; ...T2}` the environment for `T2` includes declarations from
   `T1` and in `T1 with (P = T2)` the path `P` is specific to `T1`.
   
   When defined, `T1 & T2` is always a subtype of both `T1` and `T2`
   
       T1 & T2  :>  T1
       T1 & T2  :>  T2

   

   polytypic committed Aug 24, 2020
   Configuration menu

   • View commit details
   • Copy full SHA for d0e549b
   • Browse repository at this point

   Copy the full SHA

   d0e549b View commit details

   Browse the repository at this point in the history

2. Separate matching from subtyping like in F-ing modules to allow RDS

   

   polytypic committed Aug 24, 2020
   Configuration menu

   • View commit details
   • Copy full SHA for 0778534
   • Browse repository at this point

   Copy the full SHA

   0778534 View commit details

   Browse the repository at this point in the history