From 5598b8828f5c17cc2bd035a218f2ca5cb915e323 Mon Sep 17 00:00:00 2001 From: Ikko Eltociear Ashimine Date: Sun, 28 Jul 2024 01:19:22 +0900 Subject: [PATCH] chore: update Topological.lean minor fix --- src/lake/Lake/Build/Topological.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean index ae977df7673b..d0e34890f04b 100644 --- a/src/lake/Lake/Build/Topological.lean +++ b/src/lake/Lake/Build/Topological.lean @@ -29,7 +29,7 @@ In this section, we define the primitives that make up a builder. A dependently typed monadic *fetch* function. That is, a function within the monad `m` and takes an input `a : α` -describing what to fetch and and produces some output `b : β a` (dependently +describing what to fetch and produces some output `b : β a` (dependently typed) or `b : B` (not) describing what was fetched. All build functions are fetch functions, but not all fetch functions need build something. -/