coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] print types in let bindings

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] print types in let bindings
Date: Thu, 19 Jan 2017 13:10:27 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f180.google.com
Ironport-phdr: 9a23:VQWFARZQA6aGd4nBvdBmj3//LSx+4OfEezUN459isYplN5qZr869bnLW6fgltlLVR4KTs6sC0LuK9fy5EjVYu96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52Ixi6twrcutQZjYd/Nqo91AbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRyhqRJxwJPabp+JO/dlZKzRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt5XwqEAOrRu/HgmsBP3gyjxVjXLq2601yeIhHhzb1wEnBd0Bq3TUrNTuNKcST++1z7PEwi/Fb/xM3zfy9ZLEchEgofGQUrJ9asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uRuVeWqi2E9qgFxpCCiydsrionTgIIa1FTE9SFjzIkrONK4VVZ3bsKjEJtWrCGaK5F2TtknQ2Fsvisx174IuYajcSQU1JgqwwTTZv+HfoSS/x7uVfudLS1liH9mZL6ygQu5/1K6xe3mTMa01U5HripbndnIsXAAzxnT5dKGSvt550ug2TiO2xzK5uFKPEw5lrbXJ4Quwr43kZoTvkDDETHslErqi6+Wc10o+umu6+v5frXrvoGQO5Nwhw3kMakjmtazDfk5PwQTRWSX5Oex2KH78U38WrpKj/k2kqfDsJDdIMQWvrS2DBRV0oYi8Ba/Dymp0NcCkXYdKlJKYhSHgJXzN1HPIfD4Efi/jk+jkDdu3f/GP7nhDo/RIXjElbftZax95FJEyAov0dBf4IpZBa0GIPLqQ0P+qNjYDgIiPAGv2ObmCNB91psEVm6VA6+ZNrnSsV6S6e41LemMftxdhDGoIP88ovXqkHVxzVQaZOyi2YYdQHG+BPVvZUuDNynCmNAERE4AvgslTOHpwHSEWDhfLyK7VaI9/TE2C8SvC47FSsasgaCO9Ci+F5xSIGtBDwbfQj/Ta4yYVqJUO2qpKch7n2lcWA==

Is there a switch to enable printing types of let bindings?

For example:

Definition xx :nat :=

let x:=0 in x.

When I say Print xx,

I want to see

xx = let x: nat :=0 in x

instead of

xx = let x :=0 in x

I tried "Set Printing All" (in the CoqIDE menu), but I don't see those types.

IIUC, those types are already available in the kernel (constr.ml) and the printing function discards them.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] print types in let bindings, Abhishek Anand, 01/19/2017
- Re: [Coq-Club] print types in let bindings, Hugo Herbelin, 01/20/2017