Skip to main content

Browse the archive

Revision 445254861f733c4d5a0c852383bdf9a5058086bd authored by Anish Tondwalkar on 02 May 2019, 21:18:18 UTC, committed by Anish Tondwalkar on 02 May 2019, 21:18:18 UTC 
Unfuck doctests
1 parent 097f354
Raw File
LH1424.fq 
fixpoint "--rewrite"

data Field 1 = [
       | FInt {}
     ]

define funky (ds : Field a,  kkk : a) : int = (((funky ds kkk) = (coerce (a ~ int) kkk)))

constant funky : (func(1 , [(Field @(0)); @(0); int]))

expand [1 : True; 
        2 : True;
        3 : True
        ] 

bind 1 tx   : {VV : (Field bob) | []}
bind 2 ty   : {VV : bob | []}
bind 3 fInt : {VV : Field int   | [ VV = FInt]}

constraint:
  env [1; 2]
  lhs {VV : int | [VV = (funky tx ty)]}
  rhs {VV : int | [VV = (funky tx ty)]}
  id 1 tag []

constraint:
  env [3]
  lhs {VV : int | []}
  rhs {VV : int | [4 = (funky fInt 4)]}
  id 2 tag []

constraint:
  env []
  lhs {VV : int | []}
  rhs {VV : int | [4 = (funky FInt 4)]}
  id 3 tag []
back to top