From e5118b8f206d1a6a21ab782067c8f5c6fdf293d4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 24 Nov 2023 13:13:19 +0100 Subject: [PATCH] feat: show the type of exists and fun arguments --- DocGen4/Load.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 6e1fc8a..7a6dec3 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -29,7 +29,10 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) let config := { -- TODO: parameterize maxHeartbeats maxHeartbeats := 100000000, - options := ⟨[(`pp.tagAppFns, true)]⟩, + options := ⟨[ + (`pp.tagAppFns, true), + (`pp.funBinderTypes, true) + ]⟩, -- TODO: Figure out whether this could cause some bugs fileName := default, fileMap := default,