search

anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
457 stars 53 forks source link

Isabelle/HOL translation: support polymorphic type synonyms #3040

Open lukaszcz opened 2 months ago

lukaszcz commented 2 months ago

Translate e.g.

fu (A B : Type) : Type := A -> B;

to

type_synonym ('A, 'B) fu = "'A ⇒ 'B"