michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): remove obsolete comments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-24 20:16:02 -07:00
parent 250cf70410
commit 02c22e509d
2 changed files with 0 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
tests/lean/bad2.lean
View file

@ -3,32 +3,8 @@ Variable nil {A : Type} : list A
Variable cons {A : Type} (head : A) (tail : list A) : list A Variable cons {A : Type} (head : A) (tail : list A) : list A
Definition n1 : list Int := cons (nat_to_int 10) nil Definition n1 : list Int := cons (nat_to_int 10) nil
Definition n2 : list Nat := cons 10 nil Definition n2 : list Nat := cons 10 nil
(*
The following example demonstrates that the expected type (list Int)
does not influece whether coercions are used or not.
*)
Definition n3 : list Int := cons 10 nil Definition n3 : list Int := cons 10 nil
(*
Here are some workarounds for the example above.
The 'let' construct is one of the main tools for providing
hints.
*)
Definition n3a : list Int :=
let a : Int := 10
in cons a nil
(* Solution b: we manually provide the coercion *)
Definition n3b : list Int := cons (nat_to_int 10) nil
(* The folowing example works *)
Definition n4 : list Int := nil Definition n4 : list Int := nil
(*
The following example demonstrates that we do not do type inference.
In the current implementation, we first elaborate the type and
then the body.
*)
Definition n5 : _ := cons 10 nil Definition n5 : _ := cons 10 nil
Set pp::coercion true Set pp::coercion true

2
tests/lean/bad2.lean.expected.out
View file

@ -6,8 +6,6 @@
Defined: n1 Defined: n1
Defined: n2 Defined: n2
Defined: n3 Defined: n3
Defined: n3a
Defined: n3b
Defined: n4 Defined: n4
Defined: n5 Defined: n5
Set: lean::pp::coercion Set: lean::pp::coercion