irrelevance examples

sweirich · Jun 30, 2022 · 5e1cf2a · 5e1cf2a
1 parent 5f20e2a
commit 5e1cf2a
Show file tree

Hide file tree

Showing 3 changed files with 51 additions and 3 deletions.
diff --git a/full/pi/Lec3.pi b/full/pi/Lec3.pi
@@ -1,6 +1,7 @@
 module Lec3 where
 
 -- can mark some arguments as irrelevant
+-- irrelevant parameters can only appear in types (or as part of irrelevant arguments)
 
 id : [x:Type] -> (y : x) -> x
 id = \[x] y. (y : x)
@@ -9,19 +10,34 @@ t0 = id [Bool] True
 
 t1 = id [Bool] (id [Bool] True)
 
+id2 : [x:Type] -> (y : x) -> x
+id2 = \[x] y. id [x] (y : x)
+
 --  This shouldn't type check because y is relevant
 --
+
 {-
 id' : [x:Type] -> [y:x] -> x
 id' = \[x][y]. y
 -}
 
+{-
+id2' : [x:Type] -> Type
+id2' = \[x]. id [Type] x 
+-}
+
+
+
 -----------------------------------------------------
 --  Irrelevant arguments are ignored during type equality
 
-irrelevance : (p : [i : Bool] -> Bool) -> p [False] = p [False]
+irrelevance : (p : [i : Bool] -> Bool) -> p [True] = p [False]
 irrelevance = \p . Refl
 
+
+
+
+
 -----------------------------------------------------
 -- Propositional equality is relevant
 -- Cannot ignore/erase proofs that are used for 'subst'. 

diff --git a/main/pi/Lec3.pi b/main/pi/Lec3.pi
@@ -1,6 +1,7 @@
 module Lec3 where
 
 -- can mark some arguments as irrelevant
+-- irrelevant parameters can only appear in types (or as part of irrelevant arguments)
 
 id : [x:Type] -> (y : x) -> x
 id = \[x] y. (y : x)
@@ -9,19 +10,34 @@ t0 = id [Bool] True
 
 t1 = id [Bool] (id [Bool] True)
 
+id2 : [x:Type] -> (y : x) -> x
+id2 = \[x] y. id [x] (y : x)
+
 --  This shouldn't type check because y is relevant
 --
+
 {-
 id' : [x:Type] -> [y:x] -> x
 id' = \[x][y]. y
 -}
 
+{-
+id2' : [x:Type] -> Type
+id2' = \[x]. id [Type] x 
+-}
+
+
+
 -----------------------------------------------------
 --  Irrelevant arguments are ignored during type equality
 
-irrelevance : (p : [i : Bool] -> Bool) -> p [False] = p [False]
+irrelevance : (p : [i : Bool] -> Bool) -> p [True] = p [False]
 irrelevance = \p . Refl
 
+
+
+
+
 -----------------------------------------------------
 -- Propositional equality is relevant
 -- Cannot ignore/erase proofs that are used for 'subst'. 

diff --git a/version3/pi/Lec3.pi b/version3/pi/Lec3.pi
@@ -1,6 +1,7 @@
 module Lec3 where
 
 -- can mark some arguments as irrelevant
+-- irrelevant parameters can only appear in types (or as part of irrelevant arguments)
 
 id : [x:Type] -> (y : x) -> x
 id = \[x] y. (y : x)
@@ -9,19 +10,34 @@ t0 = id [Bool] True
 
 t1 = id [Bool] (id [Bool] True)
 
+id2 : [x:Type] -> (y : x) -> x
+id2 = \[x] y. id [x] (y : x)
+
 --  This shouldn't type check because y is relevant
 --
+
 {-
 id' : [x:Type] -> [y:x] -> x
 id' = \[x][y]. y
 -}
 
+{-
+id2' : [x:Type] -> Type
+id2' = \[x]. id [Type] x 
+-}
+
+
+
 -----------------------------------------------------
 --  Irrelevant arguments are ignored during type equality
 
-irrelevance : (p : [i : Bool] -> Bool) -> p [False] = p [False]
+irrelevance : (p : [i : Bool] -> Bool) -> p [True] = p [False]
 irrelevance = \p . Refl
 
+
+
+
+
 -----------------------------------------------------
 -- Propositional equality is relevant
 -- Cannot ignore/erase proofs that are used for 'subst'.