From 56e59cd5abe444d0544b8ee95602a2197ddcb408 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Fri, 10 Jan 2025 17:22:17 -0500 Subject: [PATCH] m --- compiler/src/compiler/CustomFix.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/compiler/src/compiler/CustomFix.v b/compiler/src/compiler/CustomFix.v index ea434b8f1..20cc91f04 100644 --- a/compiler/src/compiler/CustomFix.v +++ b/compiler/src/compiler/CustomFix.v @@ -2,7 +2,7 @@ Most of the file is nearly-verbatim copied from the stdlib file where Fix_eq is proven. The main goal is to get general recursion even when some arguments to the recursive function is a function (without using funext). *) -(*Here we have, supposedly, maximum generality: dependent types and arbitrary equivalence relations*) +(*Here we have, supposedly, maximum generality: dependent types and arbitrary relations*) Section GeneralFixPoint. Variable A : Type. Variable R : A -> A -> Prop. @@ -48,7 +48,7 @@ Section GeneralFixPoint. Qed. End GeneralFixPoint. -(*Here we have equivalence relations but no dependent types.*) +(*Here we have arbitrary relations but no dependent types.*) Section NonDepFixPoint. Variable A : Type. Variable R : A -> A -> Prop. @@ -68,7 +68,7 @@ Section NonDepFixPoint. Definition Fix_eq'_nondep := Fix_eq' A R Rwf (fun _ => P) F E1 (fun _ _ => E2) F_ext. End NonDepFixPoint. -(*Here we have dependent types but equivalence relations are eq. +(*Here we have dependent types but the relations are eq. Sadly we can't simply deduce these lemmas from the supposedly-general case, since there's no good way of instantiating E2 to get eq.*) Section EqualityFixPoint.