Remove Path.inProp from prelude

JetBrains · Feb 9, 2024 · 94506bb · 94506bb
1 parent 97e2f4b
commit 94506bb
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 16 deletions.
diff --git a/api/src/main/java/org/arend/ext/ArendPrelude.java b/api/src/main/java/org/arend/ext/ArendPrelude.java
@@ -29,7 +29,6 @@ public interface ArendPrelude {
   CoreDataDefinition getPath();
   CoreFunctionDefinition getEquality();
   ArendRef getPathConRef();
-  CoreFunctionDefinition getInProp();
   CoreFunctionDefinition getIdp();
   ArendRef getAtRef();
   CoreFunctionDefinition getIso();

diff --git a/base/src/main/java/org/arend/prelude/Prelude.java b/base/src/main/java/org/arend/prelude/Prelude.java
@@ -71,8 +71,6 @@ public class Prelude implements ArendPrelude {
   public static FunctionDefinition PATH_INFIX;
   public static Constructor PATH_CON;
 
-  public static FunctionDefinition IN_PROP;
-
   public static DConstructor IDP;
   public static FunctionDefinition AT;
   public static FunctionDefinition ISO;
@@ -198,10 +196,6 @@ public static void update(Definition definition) {
         FIN_FROM_NAT = (FunctionDefinition) definition;
         FIN_FROM_NAT.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
       }
-      case "inProp" -> {
-        IN_PROP = (FunctionDefinition) definition;
-        IN_PROP.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
-      }
       case "divMod" -> {
         DIV_MOD = (FunctionDefinition) definition;
         DIV_MOD.setStatus(Definition.TypeCheckingStatus.NO_ERRORS);
@@ -269,7 +263,6 @@ public static void forEach(Consumer<Definition> consumer) {
     consumer.accept(PATH);
     consumer.accept(PATH_CON);
     consumer.accept(PATH_INFIX);
-    consumer.accept(IN_PROP);
     consumer.accept(IDP);
     consumer.accept(AT);
     consumer.accept(COERCE);
@@ -428,11 +421,6 @@ public ArendRef getPathConRef() {
     return PATH_CON.getRef();
   }
 
-  @Override
-  public FunctionDefinition getInProp() {
-    return IN_PROP;
-  }
-
   @Override
   public DConstructor getIdp() {
     return IDP;

diff --git a/lib/Prelude.ard b/lib/Prelude.ard
@@ -17,9 +17,6 @@
 
 \data Path (A : I -> \Type) (a : A left) (a' : A right)
   | path (\Pi (i : I) -> A i)
-  \where {
-    \lemma inProp {A : \Prop} : \Pi (a a' : A) -> a = a'
-  }
 
 \func \infix 1 = {A : \Type} (a a' : A) => Path (\lam _ => A) a a'