Last change
on this file since 231 was
228,
checked in by mulligan, 10 years ago

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size:
761 bytes

Line  

1  include "Bool.ma". 

2  

3  include "logic/pts.ma". 

4  include "Plogic/equality.ma". 

5  

6  ninductive Maybe (A: Type[0]): Type[0] ≝ 

7  Nothing: Maybe A 

8   Just: A → Maybe A. 

9  

10  ndefinition is_just ≝ 

11  λA: Type[0]. 

12  λm: Maybe A. 

13  match m with 

14  [ Nothing ⇒ False 

15   Just j ⇒ True 

16  ]. 

17  

18  ndefinition is_nothing ≝ 

19  λA: Type[0]. 

20  λm: Maybe A. 

21  match m with 

22  [ Nothing ⇒ True 

23   Just j ⇒ False 

24  ]. 

25  

26  ndefinition to_maybe ≝ 

27  λA: Type[0]. 

28  λb: Bool. 

29  λa: A. 

30  match b with 

31  [ True ⇒ Just A a 

32   False ⇒ Nothing A 

33  ]. 

34  

35  nlemma to_maybe_is_just: 

36  ∀A: Type[0]. 

37  ∀a: A. 

38  ∀b: Bool. 

39  is_just A (to_maybe A b a) = b. 

40  #A a b. 

41  ncases b. 

42  nnormalize. 

43  @. 

44  nnormalize. 

45  @. 

46  nqed. 

Note: See
TracBrowser
for help on using the repository browser.