michaeljklein/flock_desugar_resugar_bijection.md

## flock_desugar_resugar_bijection.md

      
    Raw
  

              flock_desugar_resugar_bijection.md
            
          
    Bijection, from very explicit to very implicit:
Bijection := '(f := _) -> '(a := _) -> '(b := _) -> '(n := _ : Nat) -> '(m := _ : Nat) -> '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(f) -> '(a) -> '(b) -> '(n : Nat) -> '(m : Nat) -> '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(f) -> '(a) -> '(b) -> '(n) -> '(m) -> '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(f : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(_ : (a :# n) -> (b :# m)) -> '(n = m)
Bijection := '(_ : (_ :# n) -> (_ :# m)) -> '(n = m)
Bijection := '(_ : (_ :# n) -> (_ :# n)) -> '(n = n)
Bijection := '((_ :# n) -> (_ :# n)) -> '(n = n)
Bijection := '((_ :# n) -> (_ :# n))
Bijection := (_ :# n) -> (_ :# n)
Bijection := _ :# n -> _ :# n

Note, this expression of bijection uses quoting, but since flock is symmetric across quoting, unquoting,
we can just as easily resugar along unquoting:
Bijection := _ :# n -> _ :# n
Bijection := (_ :# n) -> (_ :# n)
Bijection := `((_ :# n) -> (_ :# n))
Bijection := `((_ :# n) -> (_ :# n)) -> `(n = n)
Bijection := `(_ : (_ :# n) -> (_ :# n)) -> `(n = n)
Bijection := `(_ : (_ :# n) -> (_ :# m)) -> `(n = m)
Bijection := `(_ : (a :# n) -> (b :# m)) -> `(n = m)
Bijection := `(f : (a :# n) -> (b :# m)) -> `(n = m)
Bijection := `(f) -> `(a) -> `(b) -> `(n) -> `(m) -> `(f : (a :# n) -> (b :# m)) -> `(n = m)
Bijection := `(f) -> `(a) -> `(b) -> `(n : Nat) -> `(m : Nat) -> `(f : (a :# n) -> (b :# m)) -> `(n = m)
Bijection := `(f := _) -> `(a := _) -> `(b := _) -> `(n := _ : Nat) -> `(m := _ : Nat) -> `(f : (a :# n) -> (b :# m)) -> `(n = m)