Theory "one"

Parents     marker

Signature

Type Arity
one 0
Constant Type
one_case :'a -> one -> 'a
one :one

Definitions

one_TY_DEF 
|- ?rep. TYPE_DEFINITION (\b. b) rep
one_DEF 
|- () = @x. T
one_case_def 
|- !u x. (case x of () -> u) = (if x = () then u else u)

Theorems

one_axiom 
|- !f g. f = g
one 
|- !v. v = ()
one_Axiom 
|- !e. ?!fn. fn () = e
one_prim_rec 
|- !e. ?fn. fn () = e
one_induction 
|- !P. P () ==> !x. P x
one_case_rw 
|- !u x. (case x of () -> u) = u
one_case_thm 
|- !u. (case () of () -> u) = u