Quelle typing.v Sprache: Coq

Require Import Ltac2.Ltac2.

(** Ltac2 is typed à la ML. *)

Ltac2 test0 n := Int.add n 1.

Print Ltac2 test0.

Ltac2 test1 () := test0 0.

Print Ltac2 test1.

Fail Ltac2 test2 () := test0 true.

Fail Ltac2 test2 () := test0 0 0.

Ltac2 test3 f x := x, (f x, x).

Print Ltac2 test3.

(** Polymorphism *)

Ltac2 rec list_length l :=
match l with
| [] => 0
| x :: l => Int.add 1 (list_length l)
end.

Print Ltac2 list_length.

(** Pattern-matching *)

Ltac2 ifb b f g := match b with
| true => f ()
| false => g ()
end.

Print Ltac2 ifb.

Ltac2 if_not_found e f g := match e with
| Not_found => f ()
| _ => g ()
end.

Fail Ltac2 ifb' b f g := match b with
| true => f ()
end.

Fail Ltac2 if_not_found' e f g := match e with
| Not_found => f ()
end.

(** Reimplementing 'do'. Return value of the function useless. *)

Ltac2 rec do n tac := match Int.equal n 0 with
| true => ()
| false => tac (); do (Int.sub n 1) tac
end.

Print Ltac2 do.

(** Non-function pure values are OK. *)

Ltac2 tuple0 := ([1; 2], true, (fun () => "yay")).

Print Ltac2 tuple0.

(** Impure values are not. *)

Fail Ltac2 not_a_value := { contents := 0 }.
Fail Ltac2 not_a_value := "nope".
Fail Ltac2 not_a_value := list_length [].

(** Check type ascription on letrec *)

Ltac2 rec loop : 'a -> 'b := fun x => loop x.
Fail Ltac2 rec loop2 : bool -> bool := fun x => if x then loop2 false else 0.

Fail Ltac2 rec not_a_fun := ().

quality99%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.