Commit 9f6ebf75 authored by MARCHE Claude's avatar MARCHE Claude

added and ignored files

parent a0279278
......@@ -141,7 +141,9 @@ orphaned-proofs.prf
pvsbin/
# Isabelle
/lib/isabelle/bool/
/lib/isabelle/int/
/lib/isabelle/number/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/set/
......
theory Nd
use import real.Real
goal G3: forall a:real . (a > 0.0) -> (inv (a) > 0.0)
end
\ No newline at end of file
module M
type t = O | S t
let f () =
let ghost g (x:t) : t =
match x with O -> O | S y -> y end
(*
with ghost h (x:t) : t =
match x with O -> O | S y -> y end
*)
in
()
end
theory T
use import option.Option
type t 'a = A | Lam (t (option 'a))
inductive r (t 'a) (t 'a) =
| cas : forall x y:t (option 'a). r x y -> r (Lam x) (Lam y)
goal G : true
end
module M
type t = O | S t
let f () =
let ghost g (x:t) : t =
match x with O -> O | S y -> y end
(*
with ghost h (x:t) : t =
match x with O -> O | S y -> y end
*)
in
()
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment