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