summaryrefslogtreecommitdiff
path: root/Source/Dafny/RefinementTransformer.cs
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-02-02 15:36:36 -0800
committerGravatar qunyanm <unknown>2016-02-02 15:36:36 -0800
commit0d003990dd503ceb9cc56e7fb590981e752b5cfa (patch)
treedf346ae8ea4724f406a1b030ecf4b7df6a538c8d /Source/Dafny/RefinementTransformer.cs
parent2be514ca20e1478b6df02ef2b4c2725c319ac934 (diff)
Fix issue 129. When looking for a constructor for which Dafny knows how to
instantiate all it arguments, don't stop as soon as one instantiable constructor is found. Instead, figure out all instantiable constructors and then pick the best among these. A simple and reasonable "best" is an instantiable constructor that requires a minimal number of already constructed type arguments, and to break ties among these, pick the first one listed.
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
0 files changed, 0 insertions, 0 deletions