clash_axiom1.why 118 Bytes
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13

(* test file *)

theory A
  type t
  axiom Ax : forall x:t. true
end

theory B
  use export A
  axiom Ax : true
end