(* *)
(**************************************************************************)
-(* This file was generated by xoa.native: do not edit *********************)
+(* LOGIC ********************************************************************)
+
+(* NOTE: This file was generated by xoa.native, do not edit *****************)
include "basics/pts.ma".
include "ground/notation/xoa/or_3.ma".
-(* multiple disjunction connective (3) *)
-
+(* Note: multiple disjunction connective (3) *)
inductive or3 (P0,P1,P2:Prop) : Prop ≝
- | or3_intro0: P0 → or3 ? ? ?
- | or3_intro1: P1 → or3 ? ? ?
- | or3_intro2: P2 → or3 ? ? ?
+ | or3_intro0: P0 → or3 ? ? ?
+ | or3_intro1: P1 → or3 ? ? ?
+ | or3_intro2: P2 → or3 ? ? ?
.
interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).