namespace latin:/❚

fixmeta ur:?LF❚

theory PLModel =
  include ?SFOLEQND❙
  include ?Booleans❙
❚

// View currently not total

view PLSemantics : ?PLND → ?PLModel =
  prop = tm bool❙
  ded  = [F] ⊦ F ≐ tt❙
  
  true = tt❙
  false = ff❙
  
  and   = [x,y] if x then y else ff❙
  or    = [x,y] if x then tt else y❙
  impl  = [x,y] if x then y else tt❙
  not   = [x] if x then ff else tt❙
  equiv = [x,y] if x then y else if y then ff else tt❙

  trueI = refl❙
  falseE = [p][a] (bool_nontrivial notE (p sym)) inconE❙
  
  andI = [F][G][p][q]
          trans3 (p congT [u] if u then G else ff) if_tt q❙

❚