From 5e1cf2a00e19abb677f3de61c871f0cd751d299a Mon Sep 17 00:00:00 2001
From: Stephanie Weirich <sweirich@seas.upenn.edu>
Date: Thu, 30 Jun 2022 09:59:21 -0700
Subject: [PATCH] irrelevance examples

---
 full/pi/Lec3.pi     | 18 +++++++++++++++++-
 main/pi/Lec3.pi     | 18 +++++++++++++++++-
 version3/pi/Lec3.pi | 18 +++++++++++++++++-
 3 files changed, 51 insertions(+), 3 deletions(-)

diff --git a/full/pi/Lec3.pi b/full/pi/Lec3.pi
index 59e6d37..3f59a58 100644
--- 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
index 59e6d37..3f59a58 100644
--- 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
index 59e6d37..3f59a58 100644
--- 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'.