#include <stdio.h>

int main(void)
{
    __XC_UART = 1;
    U1RXRbits.U1RXR = 0b0100;
    RPB3Rbits.RPB3R = 0b0001;
    
    U1STAbits.UTXEN = 1;
    U1STAbits.URXEN = 1;
    U1BRG = 129;
    
    U1MODEbits.ON = 1;
    
    printf("Hello, world!\n");
    while(1);
}