diff options
| author | Malte Voos <git@mal.tc> | 2024-06-23 01:36:48 +0200 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-06-23 01:36:48 +0200 |
| commit | 8d40541003736d5319ec981278338e8c8c66daf6 (patch) | |
| tree | e595d0055af42b6a9d84e504befbe114a8cef5e2 /bin/main.ml | |
| parent | 36762e83887b6f917df46c5e40a11d53b697209d (diff) | |
| download | toytt-8d40541003736d5319ec981278338e8c8c66daf6.tar.gz toytt-8d40541003736d5319ec981278338e8c8c66daf6.zip | |
keep track of bound names everywhere to be able to output names instead of de bruijn indices
Diffstat (limited to 'bin/main.ml')
| -rw-r--r-- | bin/main.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/bin/main.ml b/bin/main.ml index ec5c4d2..afae47c 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -18,7 +18,7 @@ let rec repl () = let ast = parse input in let (tp, tm) = Elab.infer_toplevel ast in let value = Eval.eval ~env:Emp tm in - Format.printf "%a : %a\n%!" Syntax.Pretty.pp (Quote.quote ~size:0 value) Syntax.Pretty.pp (Quote.quote ~size:0 tp); + Format.printf "%a : %a\n%!" Syntax.Pretty.pp (Quote.quote ~size:0 value, Emp) Syntax.Pretty.pp (Quote.quote ~size:0 tp, Emp); repl () let () = |