feat: partial_fixpoint: theory

This PR adds the necessary domain theory that backs the `partial_fixpoint` feature. Part of #6355.
leanprover · Dec 30, 2024 · 3a5f0e6 · 3a5f0e6
1 parent 24a8561
commit 3a5f0e6
Show file tree

Hide file tree

Showing 3 changed files with 698 additions and 0 deletions.
diff --git a/src/Init/Internal.lean b/src/Init/Internal.lean
@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Init.Internal.Order
+
+/-!
+This directory is used for components of the standard library that are either considered
+implementation details or not yet ready for public consumption, and that should be available
+without explicit import (in contrast to `Std.Internal`)
+-/
diff --git a/src/Init/Internal/Order.lean b/src/Init/Internal/Order.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Init.Internal.Order.Basic