examples/bts/19_apply_with.mlw

   1 module I19_simplint
   2
   3   use int.Int
   4
   5   axiom H [@W:non_conservative_extension:N] : forall x y z. x < y -> y < z -> x < z
   6
   7   goal g: 0 < 2
   8
   9 end
  10
  11 module I19_simplpoly
  12
  13   type t
  14
  15   predicate r t t
  16
  17   axiom trans: forall x y z. r x y -> r y z -> r x z
  18
  19   constant a:t
  20   constant b:t
  21   constant c:t
  22
  23   axiom a1: r a b
  24
  25   axiom a2: r b c
  26
  27   goal test: r a c
  28
  29 end
  30
  31 module I19_simplpoly2
  32
  33   type t
  34   type t'
  35
  36   predicate r 'a t t
  37
  38   axiom trans: forall a:'a. forall a':'a. forall x y z. r a x y -> r a y z -> r a' x z
  39
  40   constant a:t
  41   constant b:t
  42   constant c:t
  43
  44   axiom trans_eq: forall x y z. r 4 x y -> r 5 y z -> a = z
  45
  46   axiom a1: forall x:'a. r x a b
  47
  48   axiom a2: forall x:'a. r x b c
  49
  50   (* apply trans 1,b,b does not work *)
  51
  52   goal test: r 1 a c
  53   (* apply trans with b *)
  54
  55 end