Skip to content

Commit

Permalink
changed the translation to Coq of NatLits to only use Z if the nats a…
Browse files Browse the repository at this point in the history
…re larger than 1,000
  • Loading branch information
Eddy Westbrook committed Dec 1, 2021
1 parent 8b1250e commit f83f010
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion saw-core-coq/src/Language/Coq/Pretty.hs
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ ppTerm p e =
parensIf (p > PrecLambda)
(ppTerm PrecApp tm <+> text ":" <+> ppTerm PrecApp tp)
NatLit i ->
if i > 20 then
if i > 1000 then
-- Explicitly convert from Z if an integer is too big
parensIf (p > PrecLambda) (text "Z.to_nat" <+> integer i <> text "%Z")
else
Expand Down

0 comments on commit f83f010

Please sign in to comment.