namespace http://cds.omdoc.org/urtheories❚

import rules scala://intersection.mmt.kwarc.info❚

/T   A representation of intersection types in MMT, following "Towards a Logical Framework with Intersection and Union Types" by Stolze, Liquori, Honsell, Scagnetto.❚

theory Intersection =
   include ?LF❙
   
   /T intersection type❙
   inter # 1 ∩ 2❙
   /T elements of an intersection type❙
   pair # ⟨ 1 , 2 ⟩ ❙
   /T projections from an intersection type❙
   project1 # proj1 1 ❙
   project2 # proj2 1 ❙

   rule rules?InterTerm❙
   rule rules?PairTerm❙
   rule rules?Projection1Term❙
   rule rules?Projection2Term❙
   rule rules?InterTyping❙
   rule rules?InterEqual❙
❚
   
theory IntersectionTest : ?Intersection = 
  a: type❙
  b: type❙

  /T auto-application ❙
  test : ((a ⟶ b) ∩ a) ⟶ b❘
       = [x] (proj1 x) (proj2 x)❙
  
  /T This is a negative test: it should fail with an error that $(a ⟶ b)∩(a ⟶ b)$ is not equal to $(a ⟶ b)∩a$.❙
  // test2 = test test❙
❚