#line 24 "/home/ubuntu/felix/src/packages/logic.fdoc"
  typedef bool = 2;
  type cbool = "bool" requires index TYPE_cbool;
  
  open class Bool
  {
    ctor bool:cbool="$1";
  
    Short cut and via closure
    noinline fun andthen (x: bool, y:1->bool) : bool =>
      if x then #y else false
    ;
  
    Short cut and via closure
    noinline fun orelse (x: bool, y:1->bool) : bool =>
      if x then true else #y
    ;
  
     Disjunction: logical and.
    fun land: bool * bool -> bool = "$1&&$2";      // x and y
  
    Negated and.
    fun nand: bool * bool -> bool = "!($1&&$2)";   // not (x and y)
  
    Conjunction: logical or.
    fun lor: bool * bool -> bool = "$1||$2";       // x or y
  
    Negated or.
    fun nor: bool * bool -> bool = "!($1||$2)";    // not (x or y)
  
    Logical exclusive or.
    fun xor: bool * bool -> bool = "$1!=$2";       // (x or y) and not (x and y)
  
    Logical negation.
    fun lnot: bool -> bool = "!$1";                // not x
  
    Logical implication.
    fun implies: bool * bool -> bool = "!$1||$2";  // not x or y
  
    Mutating or.
    proc |= : &bool * bool = "*$1|=$2;";
  
    Mutating and.
    proc &= : &bool * bool = "*$1&=$2;";
  
    // Elide double negations.
    //reduce dneg(x:bool): lnot (lnot x) => x;
    // Elide double negations.
    //reduce dneg(x:bool,y:bool): lnot (nand(x,y)) => land(x,y);
    // Elide double negations.
    //reduce dneg(x:bool,y:bool): lnot (nor(x,y)) => lor(x,y);
  }
  
  Standard operations on cboolean type.
  open class CBool
  {
    ctor cbool:bool="$1";
    const cfalse: cbool="false";
    const ctrue: cbool="true";
  
    Short cut and via closure
    noinline fun andthen (x: cbool, y:1->cbool) : cbool =>
      if x then #y else cfalse
    ;
  
    Short cut and via closure
    noinline fun orelse (x: cbool, y:1->cbool) : cbool =>
      if x then ctrue else #y
    ;
  
    Disjunction: logical and.
    fun land: cbool * cbool -> cbool = "$1&&$2";      // x and y
  
    Negated and.
    fun nand: cbool * cbool -> cbool = "!($1&&$2)";   // not (x and y)
  
    Conjunction: logical or.
    fun lor: cbool * cbool -> cbool = "$1||$2";       // x or y
  
    Negated or.
    fun nor: cbool * cbool -> cbool = "!($1||$2)";    // not (x or y)
  
    Logical exclusive or.
    fun xor: cbool * cbool -> cbool = "$1!=$2";       // (x or y) and not (x and y)
  
    Logical negation.
    fun lnot: cbool -> cbool = "!$1";                // not x
  
    Logical implication.
    fun implies: cbool * cbool -> cbool = "!$1||$2";  // not x or y
  
    Mutating or.
    proc |= : &cbool * cbool = "*$1|=$2;";
  
    Mutating and.
    proc &= : &cbool * cbool = "*$1&=$2;";
  
    // Elide double negations.
    //reduce dneg(x:cbool): lnot (lnot x) => x;
    // Elide double negations.
    //reduce dneg(x:cbool,y:cbool): lnot (nand(x,y)) => land(x,y);
    // Elide double negations.
    //reduce dneg(x:cbool,y:cbool): lnot (nor(x,y)) => lor(x,y);
  }
  
  
  instance FloatAddgrp[bool] {
    fun zero () => 0 :>> bool;
    fun - (x:bool) => (sub (2, caseno x)) :>> bool;
    fun + (x:bool, y:bool) : bool => (add ((caseno x , caseno y)) % 2) :>> bool;
    fun - (x:bool, y:bool) : bool => (add (2, sub(caseno x , caseno y)) % 2) :>> bool;
  }
  
  instance Str[bool] {
    Convert bool to string.
    fun str (b:bool) : string => if b then "true" else "false" endif;
  }
  
  instance Tord[bool] {
    Total ordering of bools, false < true.
    Note that x < y is equivalent to x implies y.
    fun < : bool * bool -> bool = "$1<$2";
  }
  
  open Tord[bool];
  open Show[bool];
  open Addgrp[bool];
  
  instance Str[cbool] {
    Convert cbool to string.
    fun str (b:cbool) : string => if b then "ctrue" else "cfalse" endif;
  }
  
  instance Tord[cbool] {
    Total ordering of cbools, false < true.
    Note that x < y is equivalent to x implies y.
    fun < : cbool * cbool -> cbool = "$1<$2";
  }
  
  open Tord[cbool];
  open Show[cbool];