blob: 9598a5979c660bb03f7cae42cbad6c52d4dabee3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import Ltac2.Ltac2.
#[deprecated(note="test_definition")]
Ltac2 foo := ().
#[deprecated(note="test_notation")]
Ltac2 Notation bar := ().
#[deprecated(note="test_external")]
Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length".
(* Randomly picked external function *)
Ltac2 Eval foo.
Ltac2 Eval bar.
Ltac2 Eval qux.
|
