From 70f86f6e93856ee7e57ed6c0e24c184fd66d0615 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 14:34:15 -0800 Subject: [PATCH] doc: Update delation documentation --- Pantograph/Delate.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index c5954f0..a4f20d7 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -1,7 +1,5 @@ /- -All serialisation functions; -This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without -using `Scope`s. +This file handles "Delation": The conversion of Kernel view into Search view. -/ import Lean import Pantograph.Expr